# Library Topology.SeparatednessAxioms

Require Export TopologicalSpaces.
Require Import InteriorsClosures.

Definition T0_sep (X:TopologicalSpace) : Prop :=
x y:point_set X, x y
( U:Ensemble (point_set X), open U In U x ¬ In U y)
( U:Ensemble (point_set X), open U ¬ In U x In U y).

Definition T1_sep (X:TopologicalSpace) : Prop :=
x:point_set X, closed (Singleton x).

Definition Hausdorff (X:TopologicalSpace) : Prop :=
x y:point_set X, x y
U:Ensemble (point_set X),
V:Ensemble (point_set X),
open U open V In U x In V y
Intersection U V = Empty_set.
Definition T2_sep := Hausdorff.

Definition T3_sep (X:TopologicalSpace) : Prop :=
T1_sep X
(x:point_set X) (F:Ensemble (point_set X)),
closed F¬ In F x U:Ensemble (point_set X),
V:Ensemble (point_set X),
open U open V In U x Included F V
Intersection U V = Empty_set.

Definition normal_sep (X:TopologicalSpace) : Prop :=
T1_sep X
(F G:Ensemble (point_set X)),
closed Fclosed GIntersection F G = Empty_set
U:Ensemble (point_set X), V:Ensemble (point_set X),
open U open V Included F U Included G V
Intersection U V = Empty_set.
Definition T4_sep := normal_sep.

Lemma T1_sep_impl_T0_sep: X:TopologicalSpace,
T1_sep XT0_sep X.
Proof.
intros.
red; intros.
left.
(Complement (Singleton y)); repeat split.
apply H.
repeat red; intro.
red; intro.
repeat red in H1.
apply H1; constructor.
Qed.

Lemma Hausdorff_impl_T1_sep: X:TopologicalSpace,
Hausdorff XT1_sep X.
Proof.
intros.
red; intros.
assert (closure (Singleton x) = Singleton x).
apply Extensionality_Ensembles; split.
red; intros.
assert (x = x0).
apply NNPP.
red; intro.
pose proof (H x x0 H1).
destruct H2 as [U [V ?]].
intuition.
assert (In (interior (Complement (Singleton x))) x0).
V.
constructor; split; trivial.
red; intros.
red; red; intro.
destruct H8.
assert (In Empty_set x).
rewrite <- H7.
constructor; trivial.
destruct H8.
assumption.
rewrite interior_complement in H6.
destruct H1; constructor.
apply closure_inflationary.

rewrite <- H0; apply closure_closed.
Qed.

Lemma T3_sep_impl_Hausdorff: X:TopologicalSpace,
T3_sep XHausdorff X.
Proof.
intros.
destruct H.
red; intros.
pose proof (H0 x (Singleton y)).
match type of H2 with | ?A → ?B → ?Cassert C end.
apply H2.
apply H.
red; intro.
destruct H3.
destruct H3 as [U [V [? [? [? [? ?]]]]]].
U; V; repeat split; auto with sets.
Qed.

Lemma normal_sep_impl_T3_sep: X:TopologicalSpace,
normal_sep XT3_sep X.
Proof.
intros.
destruct H.
split; trivial.
intros.
pose proof (H0 (Singleton x) F).
match type of H3 with | ?A → ?B → ?C → ?Dassert D end.
apply H3; trivial.
apply Extensionality_Ensembles; split; auto with sets.
red; intros.
destruct H4 as [? []].
destruct H4 as [U [V [? [? [? [? ?]]]]]].
U; V; repeat split; auto with sets.
Qed.

Section Hausdorff_and_nets.
Require Export Nets.

Lemma Hausdorff_impl_net_limit_unique:
{X:TopologicalSpace} {I:DirectedSet} (x:Net I X),
Hausdorff Xuniqueness (net_limit x).
Proof.
intros.
red; intros x1 x2 ? ?.
apply NNPP; intro.
destruct (H x1 x2) as [U [V [? [? [? [? ?]]]]]]; trivial.
destruct (H0 U H3 H5) as [i].
destruct (H1 V H4 H6) as [j].
destruct (DS_join_cond i j) as [k [? ?]].
assert (In (Intersection U V) (x k)).
constructor; (apply H8 || apply H9); trivial.
rewrite H7 in H12.
destruct H12.
Qed.

Lemma Hausdorff_impl_net_limit_is_unique_cluster_point:
{X:TopologicalSpace} {I:DirectedSet} (x:Net I X)
(x0:point_set X), Hausdorff Xnet_limit x x0
y:point_set X, net_cluster_point x yy = x0.
Proof.
intros.
destruct (net_cluster_point_impl_subnet_converges _ _ x y H1) as
[J [x' [? ?]]].
destruct (H0 Full_set).
apply open_full.
constructor.
; exact x1.
assert (net_limit x' x0).
apply subnet_limit with _ x; trivial.
apply Hausdorff_impl_net_limit_unique with x'; trivial.
Qed.

Lemma net_limit_is_unique_cluster_point_impl_Hausdorff:
(X:TopologicalSpace),
( (I:DirectedSet) (x:Net I X) (x0 y:point_set X),
net_limit x x0net_cluster_point x y
y = x0) → Hausdorff X.
Proof.
intros.
red; intros.
assert (¬ net_cluster_point (neighborhood_net _ x) y).
red; intro.
symmetry.
apply H with _ (neighborhood_net _ x).
apply neighborhood_net_limit.
assumption.

apply not_all_ex_not in H1.
destruct H1 as [V].
apply imply_to_and in H1.
destruct H1.
apply imply_to_and in H2.
destruct H2.
apply not_all_ex_not in H3.
destruct H3 as [[U]].
U; V; repeat split; trivial.
apply Extensionality_Ensembles; split; auto with sets.
red; intros.
destruct H4.
(intro_neighborhood_net_DS X x U x0 o i H4).
split.
simpl; auto with sets.
simpl.
trivial.
Qed.

Lemma net_limit_uniqueness_impl_Hausdorff:
X:TopologicalSpace,
( (I:DirectedSet) (x:Net I X), uniqueness (net_limit x)) →
Hausdorff X.
Proof.
intros.
apply net_limit_is_unique_cluster_point_impl_Hausdorff.
intros.
pose proof (net_cluster_point_impl_subnet_converges _ _ _ _ H1).
destruct H2 as [J [x' [? ?]]].
destruct (H0 Full_set).
apply open_full.
constructor.
; exact x1.
assert (net_limit x' x0).
apply subnet_limit with _ x; trivial.
unfold uniqueness in H.
apply H with _ x'; trivial.
Qed.

End Hausdorff_and_nets.