位相空間

位相空間を定義する。

Require Import category.
Require Import classical_logic.
Require Import logic.
Require Import power.
Require Import function.

Set Implicit Arguments.

定義

型 A 上の位相構造を以下のように定義する。

Record is_topology
  (A : Type)
  (is_open  : power A -> Prop)
  : Prop :=
  make_is_topology {
    top_open : is_open whole_set;

    bin_inter_open {U V} :
      is_open U ->
      is_open V ->
      is_open (U ∩ V);

    union_open {X : power (power A)} :
      (forall U, U ∈ X -> is_open U) ->
      is_open (⋃ X);
  }.

Record topology (A : Type) : Type :=
  make_topology {
    is_open : power A -> Prop;
    is_open_is_topology :> is_topology is_open;
  }.

位相構造は、A の元の集合がどのようなときに開集合であるかを is_open という述語によって指定する。A の元全体の集合は開集合である。開集合は2項の共通集合と、一般の合併によって閉じている。

位相空間とは、型とその上の位相の組である。

Record topological_space : Type :=
  make_topological_space {
    A :> Type;
    topology_on_A :> topology A;
  }.

閉集合を定義する。

Definition is_closed
  (X : topological_space)
  (S : power X)
  : Prop
  := X.(is_open) (complement S).

Lemma empty_open
  (X : topological_space)
  : X.(is_open) empty_set.
X: topological_space
is_open X empty_set
Proof.
X: topological_space
is_open X empty_set
  rewrite<- union_of_empty_set.
X: topological_space
is_open X (⋃ empty_set)
  apply X.(union_open).
X: topological_space
forall U : power X, U ∈ empty_set -> is_open X U
  intros.
X: topological_space
U: power X
H: U ∈ empty_set
is_open X U
  unfold mem, empty_set in H.
X: topological_space
U: power X
H: False
is_open X U
  contradiction.
Qed.

例

どんな型も、その上に離散位相を考えることができる。

Definition discrete_topology (A : Type) : topology A.
A: Type
topology A
Proof.
A: Type
topology A
  exists (fun S => True).
A: Type
is_topology (fun _ : power A => True)
  constructor.
A: Type
True
A: Type
power A -> power A -> True -> True -> True
A: Type
forall X : power (power A), (forall U : power A, U ∈ X -> True) -> True
  -
A: Type
True
    simpl.
A: Type
True
    trivial.
  -
A: Type
power A -> power A -> True -> True -> True
    simpl.
A: Type
power A -> power A -> True -> True -> True
    trivial.
  -
A: Type
forall X : power (power A), (forall U : power A, U ∈ X -> True) -> True
    simpl.
A: Type
forall X : power (power A), (forall U : power A, U ∈ X -> True) -> True
    trivial.
Defined.

どんな型も、その上に密着位相を考えることができる。

Lemma indiscrete_topology_is_topology
  (A : Type)
  : is_topology (fun S : power A => S = empty_set \/ S = whole_set).
A: Type
is_topology (fun S : power A => S = empty_set \/ S = whole_set)
Proof.
A: Type
is_topology (fun S : power A => S = empty_set \/ S = whole_set)
  constructor.
A: Type
whole_set = empty_set \/ whole_set = whole_set
A: Type
forall U V : power A,
U = empty_set \/ U = whole_set ->
V = empty_set \/ V = whole_set -> U ∩ V = empty_set \/ U ∩ V = whole_set
A: Type
forall X : power (power A),
(forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set) ->
⋃ X = empty_set \/ ⋃ X = whole_set

まず whole_set が開集合であることを示す。

  -
A: Type
whole_set = empty_set \/ whole_set = whole_set
    right.
A: Type
whole_set = whole_set
    reflexivity.

次に2項の共通集合で閉じていることを示す。

  -
A: Type
forall U V : power A,
U = empty_set \/ U = whole_set ->
V = empty_set \/ V = whole_set -> U ∩ V = empty_set \/ U ∩ V = whole_set
    intros.
A: Type
U, V: power A
H: U = empty_set \/ U = whole_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
    destruct H.
A: Type
U, V: power A
H: U = empty_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
A: Type
U, V: power A
H: U = whole_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
    +
A: Type
U, V: power A
H: U = empty_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
      left.
A: Type
U, V: power A
H: U = empty_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set
      subst U.
A: Type
V: power A
H0: V = empty_set \/ V = whole_set
empty_set ∩ V = empty_set
      apply bin_inter_empty_set_left.
    +
A: Type
U, V: power A
H: U = whole_set
H0: V = empty_set \/ V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
      destruct H0.
A: Type
U, V: power A
H: U = whole_set
H0: V = empty_set
U ∩ V = empty_set \/ U ∩ V = whole_set
A: Type
U, V: power A
H: U = whole_set
H0: V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
      *
A: Type
U, V: power A
H: U = whole_set
H0: V = empty_set
U ∩ V = empty_set \/ U ∩ V = whole_set
        left.
A: Type
U, V: power A
H: U = whole_set
H0: V = empty_set
U ∩ V = empty_set
        subst V.
A: Type
U: power A
H: U = whole_set
U ∩ empty_set = empty_set
        apply bin_inter_empty_set_right.
      *
A: Type
U, V: power A
H: U = whole_set
H0: V = whole_set
U ∩ V = empty_set \/ U ∩ V = whole_set
        right.
A: Type
U, V: power A
H: U = whole_set
H0: V = whole_set
U ∩ V = whole_set
        subst U V.
A: Type
whole_set ∩ whole_set = whole_set
        apply bin_inter_left_unit.

最後に任意の合併で閉じていることを示す。

  -
A: Type
forall X : power (power A),
(forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set) ->
⋃ X = empty_set \/ ⋃ X = whole_set
    intros.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
⋃ X = empty_set \/ ⋃ X = whole_set
    destruct (exists_or_none (fun U => U ∈ X /\ U = whole_set)).
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: exists x : power A, x ∈ X /\ x = whole_set
⋃ X = empty_set \/ ⋃ X = whole_set
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
⋃ X = empty_set \/ ⋃ X = whole_set
    +
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: exists x : power A, x ∈ X /\ x = whole_set
⋃ X = empty_set \/ ⋃ X = whole_set
      right.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: exists x : power A, x ∈ X /\ x = whole_set
⋃ X = whole_set
      destruct H0 as [U [H1 H2]].
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
U: power A
H1: U ∈ X
H2: U = whole_set
⋃ X = whole_set
      rewrite H2 in H1.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
U: power A
H1: whole_set ∈ X
H2: U = whole_set
⋃ X = whole_set
      apply (union_whole_set H1).
    +
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
⋃ X = empty_set \/ ⋃ X = whole_set
      left.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
⋃ X = empty_set
      apply subset_of_empty_set.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
⋃ X ⊆ empty_set
      apply union_least_upper_bound.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
forall S : power A, S ∈ X -> S ⊆ empty_set
      intros.
A: Type
X: power (power A)
H: forall U : power A, U ∈ X -> U = empty_set \/ U = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
S: power A
H1: S ∈ X
S ⊆ empty_set
      specialize (H S H1).
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H0: forall x : power A, ~ (x ∈ X /\ x = whole_set)
H1: S ∈ X
S ⊆ empty_set
      specialize (H0 S).
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H0: ~ (S ∈ X /\ S = whole_set)
H1: S ∈ X
S ⊆ empty_set
      assert (S <> whole_set) by
        exact (uncurry_not H0 H1).
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H0: ~ (S ∈ X /\ S = whole_set)
H1: S ∈ X
H2: S <> whole_set
S ⊆ empty_set
      clear H0 H1.
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H2: S <> whole_set
S ⊆ empty_set
      apply (disj_delete_right H) in H2.
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H2: S = empty_set
S ⊆ empty_set
      rewrite H2.
A: Type
X: power (power A)
S: power A
H: S = empty_set \/ S = whole_set
H2: S = empty_set
empty_set ⊆ empty_set
      apply inclusion_refl.
Qed.

これで離散位相が実際に位相であることが分かった。

Definition indiscrete_topology (A : Type) : topology A.
A: Type
topology A
Proof.
A: Type
topology A
  exists (fun S => S = empty_set \/ S = whole_set).
A: Type
is_topology (fun S : power A => S = empty_set \/ S = whole_set)
  apply indiscrete_topology_is_topology.
Defined.

Print indiscrete_topology.
indiscrete_topology =
fun A : Type =>
{|
  is_open := fun S : power A => S = empty_set \/ S = whole_set;
  is_open_is_topology := indiscrete_topology_is_topology A
|}
     : forall A : Type, topology A

Arguments indiscrete_topology A%_type_scope

連続写像

Definition continuous
  {A B}
  (X : topology A)
  (Y : topology B)
  (f : A -> B)
  : Prop :=
  forall U : power B,
    Y.(is_open _) U ->
    X.(is_open _) (preimage f U).

Record continuous_map
  (X Y : topological_space)
  : Type :=
  make_continuous_map {
    f :> X -> Y;
    f_is_continous :> continuous X Y f;
  }.

Lemma identity_continuous
  {A}
  (X : topology A)
  : continuous X X id_function.
A: Type
X: topology A
continuous X X id_function
Proof.
A: Type
X: topology A
continuous X X id_function
  unfold continuous.
A: Type
X: topology A
forall U : power A, is_open X U -> is_open X (preimage id_function U)
  intros.
A: Type
X: topology A
U: power A
H: is_open X U
is_open X (preimage id_function U)
  unfold preimage.
A: Type
X: topology A
U: power A
H: is_open X U
is_open X (fun a : A => U (id_function a))
  assumption.
Qed.

Definition identity_continuous_map
  (X : topological_space)
  : continuous_map X X.
X: topological_space
continuous_map X X
Proof.
X: topological_space
continuous_map X X
  exists id_function.
X: topological_space
continuous X X id_function
  apply identity_continuous.
Defined.

Lemma composition_continuous
  {A B C}
  {X : topology A}
  {Y : topology B}
  {Z : topology C}
  {f : A -> B}
  {g : B -> C}
  (g' : continuous Y Z g)
  (f' : continuous X Y f)
  : continuous X Z (compose_functions g f).
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
continuous X Z (compose_functions g f)
Proof.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
continuous X Z (compose_functions g f)
  unfold continuous.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
forall U : power C,
is_open Z U -> is_open X (preimage (compose_functions g f) U)
  intros.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
U: power C
H: is_open Z U
is_open X (preimage (compose_functions g f) U)
  rewrite preimage_of_composition.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
U: power C
H: is_open Z U
is_open X (preimage f (preimage g U))
  apply f'.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
U: power C
H: is_open Z U
is_open Y (preimage g U)
  apply g'.
A, B, C: Type
X: topology A
Y: topology B
Z: topology C
f: A -> B
g: B -> C
g': continuous Y Z g
f': continuous X Y f
U: power C
H: is_open Z U
is_open Z U
  assumption.
Qed.

Definition composition_continuous_map
  {X Y Z : topological_space}
  (g : continuous_map Y Z)
  (f : continuous_map X Y)
  : continuous_map X Z.
X, Y, Z: topological_space
g: continuous_map Y Z
f: continuous_map X Y
continuous_map X Z
Proof.
X, Y, Z: topological_space
g: continuous_map Y Z
f: continuous_map X Y
continuous_map X Z
  exists (compose_functions g f).
X, Y, Z: topological_space
g: continuous_map Y Z
f: continuous_map X Y
continuous X Z (compose_functions g f)
  apply (composition_continuous g f).
Defined.

位相空間の圏

Definition displayed_category_of_topological_spaces_data
  : displayed_category_data category_of_types_data.
displayed_category_data category_of_types_data
Proof.
displayed_category_data category_of_types_data
  unshelve econstructor.
category_of_types_data -> Type
forall a b : category_of_types_data,
category_of_types_data [a, b] -> ?d_ob a -> ?d_ob b -> Type
forall (a : category_of_types_data) (x : ?d_ob a), ?d_hom a a id x x
forall (a b c : category_of_types_data) (x : ?d_ob a) 
  (y : ?d_ob b) (z : ?d_ob c) (g : category_of_types_data [b, c])
  (f0 : category_of_types_data [a, b]),
?d_hom b c g y z -> ?d_hom a b f0 x y -> ?d_hom a c (g ∘ f0) x z
  -
category_of_types_data -> Type
    exact topology.
  -
forall a b : category_of_types_data,
category_of_types_data [a, b] -> topology a -> topology b -> Type
    intros A B f X Y.
A, B: category_of_types_data
f: category_of_types_data [A, B]
X: topology A
Y: topology B
Type
    exact (continuous X Y f).
  -
forall (a : category_of_types_data) (x : topology a),
(fun (A0 B : category_of_types_data) (f0 : category_of_types_data [A0, B])
   (X : topology A0) (Y : topology B) =>
 continuous X Y f0) a a id x x
    simpl.
forall (a : Type) (x : topology a), continuous x x (fun x0 : a => x0)
    intros.
a: Type
x: topology a
continuous x x (fun x0 : a => x0)
    apply identity_continuous.
  -
forall (a b c : category_of_types_data) (x : topology a) 
  (y : topology b) (z : topology c) (g : category_of_types_data [b, c])
  (f0 : category_of_types_data [a, b]),
(fun (A B : category_of_types_data) (f : category_of_types_data [A, B])
   (X : topology A) (Y : topology B) =>
 continuous X Y f) b c g y z ->
(fun (A B : category_of_types_data) (f : category_of_types_data [A, B])
   (X : topology A) (Y : topology B) =>
 continuous X Y f) a b f0 x y ->
(fun (A0 B : category_of_types_data) (f1 : category_of_types_data [A0, B])
   (X : topology A0) (Y : topology B) =>
 continuous X Y f1) a c (g ∘ f0) x z
    simpl.
forall (a b c : Type) (x : topology a) (y : topology b) 
  (z : topology c) (g : b -> c) (f0 : a -> b),
continuous y z g ->
continuous x y f0 -> continuous x z (fun x0 : a => g (f0 x0))
    intros.
a, b, c: Type
x: topology a
y: topology b
z: topology c
g: b -> c
f0: a -> b
g': continuous y z g
f': continuous x y f0
continuous x z (fun x0 : a => g (f0 x0))
    apply (composition_continuous g' f').
Defined.

Print displayed_category_of_topological_spaces_data.
displayed_category_of_topological_spaces_data =
{|
  d_ob := topology;
  d_hom :=
    fun (A B : category_of_types_data) (f : category_of_types_data [A, B])
      (X : topology A) (Y : topology B) =>
    continuous X Y f;
  d_identity :=
    (fun (a : Type) (x : topology a) => identity_continuous x)
    :
    forall (a : category_of_types_data) (x : topology a),
    (fun (A B : category_of_types_data) (f : category_of_types_data [A, B])
       (X : topology A) (Y : topology B) =>
     continuous X Y f) a a id x x;
  d_comp :=
    (fun (a b c : Type) (x : topology a) (y : topology b) 
       (z : topology c) (g : b -> c) (f : a -> b) 
       (g' : continuous y z g) (f' : continuous x y f) =>
     composition_continuous g' f')
    :
    forall (a b c : category_of_types_data) (x : topology a) 
      (y : topology b) (z : topology c) (g : category_of_types_data [b, c])
      (f : category_of_types_data [a, b]),
    (fun (A B : category_of_types_data) (f0 : category_of_types_data [A, B])
       (X : topology A) (Y : topology B) =>
     continuous X Y f0) b c g y z ->
    (fun (A B : category_of_types_data) (f0 : category_of_types_data [A, B])
       (X : topology A) (Y : topology B) =>
     continuous X Y f0) a b f x y ->
    (fun (A B : category_of_types_data) (f0 : category_of_types_data [A, B])
       (X : topology A) (Y : topology B) =>
     continuous X Y f0) a c (g ∘ f) x z
|}
     : displayed_category_data category_of_types_data

近傍

Section Neighborhoods.
  Context {X : topological_space}.

  Definition neighborhood
    (x : X)
    (N : power X)
    : Prop :=
    exists U,
    X.(is_open) U /\
    x ∈ U /\
    U ⊆ N.

  Definition open_neighborhood
    (x : X)
    (U : power X)
    : Prop :=
    X.(is_open) U /\
    x ∈ U.

  Lemma open_neighborhood_is_neighborhood
    (x : X)
    (U : power X)
    : open_neighborhood x U -> neighborhood x U.
X: topological_space
x: X
U: power X
open_neighborhood x U -> neighborhood x U
  Proof.
X: topological_space
x: X
U: power X
open_neighborhood x U -> neighborhood x U
    intro.
X: topological_space
x: X
U: power X
H: open_neighborhood x U
neighborhood x U
    destruct H.
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
neighborhood x U
    exists U.
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
is_open X U /\ x ∈ U /\ U ⊆ U
    repeat split.
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
is_open X U
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
x ∈ U
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
U ⊆ U
    -
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
is_open X U
      assumption.
    -
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
x ∈ U
      assumption.
    -
X: topological_space
x: X
U: power X
H: is_open X U
H0: x ∈ U
U ⊆ U
      apply inclusion_refl.
  Qed.

  Lemma open_neighborhood_is_open_neighborhood
    (x : X)
    (U : power X) :
    X.(is_open) U ->
    neighborhood x U ->
    open_neighborhood x U.
X: topological_space
x: X
U: power X
is_open X U -> neighborhood x U -> open_neighborhood x U
  Proof.
X: topological_space
x: X
U: power X
is_open X U -> neighborhood x U -> open_neighborhood x U
    intros.
X: topological_space
x: X
U: power X
H: is_open X U
H0: neighborhood x U
open_neighborhood x U
    destruct H0 as [H0 [H1 [H2 H3]]].
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
open_neighborhood x U
    split.
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
is_open X U
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
x ∈ U
    -
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
is_open X U
      assumption.
    -
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
x ∈ U
      apply H3.
X: topological_space
x: X
U: power X
H: is_open X U
H0: power X
H1: is_open X H0
H2: x ∈ H0
H3: H0 ⊆ U
x ∈ H0
      assumption.
  Qed.
End Neighborhoods.

分離公理

Definition T1_space (X : topological_space)
  : Prop :=
  forall x : X, is_closed X (singleton x).

Definition hausdorff (X : topological_space)
  : Prop :=
  forall x y : X,
  x <> y ->
  exists U V,
  open_neighborhood x U /\
  open_neighborhood y V /\
  disjoint U V.

Lemma T1_space_separated_by_open_neighborhood
  (X : topological_space) :
  T1_space X ->
  (
    forall (x y : X),
    x <> y ->
    exists N,
    open_neighborhood x N /\
    ~ (y ∈ N)
  ).
X: topological_space
T1_space X ->
forall x y : X,
x <> y -> exists N : power X, open_neighborhood x N /\ ~ y ∈ N
Proof.
X: topological_space
T1_space X ->
forall x y : X,
x <> y -> exists N : power X, open_neighborhood x N /\ ~ y ∈ N
  intros.
X: topological_space
H: T1_space X
x, y: X
H0: x <> y
exists N : power X, open_neighborhood x N /\ ~ y ∈ N
  specialize (H y).
X: topological_space
y: X
H: is_closed X (singleton y)
x: X
H0: x <> y
exists N : power X, open_neighborhood x N /\ ~ y ∈ N
  unfold is_closed in H.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
exists N : power X, open_neighborhood x N /\ ~ y ∈ N
  exists (complement (singleton y)).
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
open_neighborhood x (complement (singleton y)) /\
~ y ∈ complement (singleton y)
  split.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
open_neighborhood x (complement (singleton y))
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
~ y ∈ complement (singleton y)
  -
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
open_neighborhood x (complement (singleton y))
    split.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
is_open X (complement (singleton y))
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
x ∈ complement (singleton y)
    +
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
is_open X (complement (singleton y))
      assumption.
    +
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
x ∈ complement (singleton y)
      unfold singleton, complement, mem.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
x <> y
      assumption.
  -
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
~ y ∈ complement (singleton y)
    unfold singleton, complement, mem.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
~ y <> y
    apply double_negation_introduction.
X: topological_space
y: X
H: is_open X (complement (singleton y))
x: X
H0: x <> y
y = y
    reflexivity.
Qed.

TODO: 以下の証明は明らかに読みにくい：

Lemma separated_by_neighborhood_T1_space
  (X : topological_space) :
  (
    forall (x y : X),
    x <> y ->
    exists N,
    neighborhood x N /\
    ~ (y ∈ N)
  ) ->
  T1_space X.
X: topological_space
(forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N) ->
T1_space X
Proof.
X: topological_space
(forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N) ->
T1_space X
  intro.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
T1_space X
  unfold T1_space.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
forall x : X, is_closed X (singleton x)
  unfold is_closed.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
forall x : X, is_open X (complement (singleton x))
  intro x.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
is_open X (complement (singleton x))

  assert (X.(is_open) (⋃ (fun S => X.(is_open) S /\ ~ (x ∈ S)))).
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
is_open X (complement (singleton x))

  -
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
    apply X.(union_open).
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
forall U : power X,
U ∈ (fun S : power X => is_open X S /\ ~ x ∈ S) -> is_open X U
    unfold mem.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
forall U : power X, is_open X U /\ ~ U x -> is_open X U
    intros.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
U: power X
H0: is_open X U /\ ~ U x
is_open X U
    destruct H0.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
U: power X
H0: is_open X U
H1: ~ U x
is_open X U
    assumption.
  -
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
is_open X (complement (singleton x))
    assert (
      complement (singleton x) =
      ⋃ (fun S => X.(is_open) S /\ ~ (x ∈ S))
    ).
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
complement (singleton x) = ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: complement (singleton x) = ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
is_open X (complement (singleton x))
    +
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
complement (singleton x) = ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
      apply inclusion_antisymmetric.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
complement (singleton x) ⊆ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
⋃ (fun S : power X => is_open X S /\ ~ x ∈ S) ⊆ complement (singleton x)
      *
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
complement (singleton x) ⊆ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        intros y H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
H1: y ∈ complement (singleton x)
y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        unfold singleton, complement, mem in H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
H1: y <> x
y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        specialize (H y x H1).
X: topological_space
x, y: X
H: exists N : power X, neighborhood y N /\ ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        destruct H as [N [H H2]].
X: topological_space
x, y: X
N: power X
H: neighborhood y N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        destruct H as [U [H [H3 H4]]].
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
        exists U.
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
U ∈ (fun S : power X => is_open X S /\ ~ x ∈ S) /\ y ∈ U
        repeat split.
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
is_open X U
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
~ x ∈ U
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
y ∈ U
        **
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
is_open X U
           assumption.
        **
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
~ x ∈ U
           intro.
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
H5: x ∈ U
False
           apply H2.
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
H5: x ∈ U
x ∈ N
           apply H4.
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
H5: x ∈ U
x ∈ U
           assumption.
        **
X: topological_space
x, y: X
N, U: power X
H: is_open X U
H3: y ∈ U
H4: U ⊆ N
H2: ~ x ∈ N
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: y <> x
y ∈ U
           assumption.
      *
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
⋃ (fun S : power X => is_open X S /\ ~ x ∈ S) ⊆ complement (singleton x)
        intros y H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
H1: y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
y ∈ complement (singleton x)
        unfold singleton, complement, mem.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
H1: y ∈ ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
y <> x
        destruct H1 as [U [H1 H2]].
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
U: power X
H1: U ∈ (fun S : power X => is_open X S /\ ~ x ∈ S)
H2: y ∈ U
y <> x
        intro.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
y: X
U: power X
H1: U ∈ (fun S : power X => is_open X S /\ ~ x ∈ S)
H2: y ∈ U
H3: y = x
False
        subst y.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
U: power X
H1: U ∈ (fun S : power X => is_open X S /\ ~ x ∈ S)
H2: x ∈ U
False
        unfold mem in H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
U: power X
H1: is_open X U /\ ~ U x
H2: x ∈ U
False
        destruct H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
U: power X
H1: is_open X U
H3: ~ U x
H2: x ∈ U
False
        apply H3.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
U: power X
H1: is_open X U
H3: ~ U x
H2: x ∈ U
U x
        assumption.
    +
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: complement (singleton x) = ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
is_open X (complement (singleton x))
      rewrite H1.
X: topological_space
H: forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
x: X
H0: is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
H1: complement (singleton x) = ⋃ (fun S : power X => is_open X S /\ ~ x ∈ S)
is_open X (⋃ (fun S : power X => is_open X S /\ ~ x ∈ S))
      apply H0.
Qed.

Lemma hausdorff_is_T1
  (X : topological_space)
  : hausdorff X -> T1_space X.
X: topological_space
hausdorff X -> T1_space X
Proof.
X: topological_space
hausdorff X -> T1_space X
  intro H.
X: topological_space
H: hausdorff X
T1_space X
  apply separated_by_neighborhood_T1_space.
X: topological_space
H: hausdorff X
forall x y : X, x <> y -> exists N : power X, neighborhood x N /\ ~ y ∈ N
  intros.
X: topological_space
H: hausdorff X
x, y: X
H0: x <> y
exists N : power X, neighborhood x N /\ ~ y ∈ N
  specialize (H x y H0).
X: topological_space
x, y: X
H: exists U V : power X,
  open_neighborhood x U /\ open_neighborhood y V /\ disjoint U V
H0: x <> y
exists N : power X, neighborhood x N /\ ~ y ∈ N
  destruct H as [U [V [H [H1 H2]]]].
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
exists N : power X, neighborhood x N /\ ~ y ∈ N
  exists U.
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
neighborhood x U /\ ~ y ∈ U
  split.
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
neighborhood x U
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
~ y ∈ U
  -
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
neighborhood x U
    apply open_neighborhood_is_neighborhood.
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
open_neighborhood x U
    assumption.
  -
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
~ y ∈ U
    intro.
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: disjoint U V
H0: x <> y
H3: y ∈ U
False
    unfold disjoint in H2.
X: topological_space
x, y: X
U, V: power X
H: open_neighborhood x U
H1: open_neighborhood y V
H2: forall x : X, x ∈ U -> x ∈ V -> False
H0: x <> y
H3: y ∈ U
False
    destruct H.
X: topological_space
x, y: X
U, V: power X
H: is_open X U
H4: x ∈ U
H1: open_neighborhood y V
H2: forall x : X, x ∈ U -> x ∈ V -> False
H0: x <> y
H3: y ∈ U
False
    destruct H1.
X: topological_space
x, y: X
U, V: power X
H: is_open X U
H4: x ∈ U
H1: is_open X V
H5: y ∈ V
H2: forall x : X, x ∈ U -> x ∈ V -> False
H0: x <> y
H3: y ∈ U
False
    specialize (H2 y H3 H5).
X: topological_space
x, y: X
U, V: power X
H: is_open X U
H4: x ∈ U
H1: is_open X V
H5: y ∈ V
H2: False
H0: x <> y
H3: y ∈ U
False
    assumption.
Qed.