# Library Coqtail.Topology.Topology

Require Import Ensembles.
Require Import Powerset.

# Infinite Union

Inductive Infinite_Union (U:Type) (I:Type) (Ai : IEnsemble U) : Ensemble U :=
Infinite_Union_intro : x:U,
( i:I, In _ (Ai i) x) →
In _ (Infinite_Union U I Ai) x.

# Topological space

Class Topological_Space
(X:Type)
(set : Ensemble X)
(topology : Ensemble (Ensemble _))
:= {
open_empty_set : In (Ensemble X) topology (Empty_set X);

open_full_set : In (Ensemble X) topology set;

intersection_stable : A B : Ensemble X,
In (Ensemble X) topology A
In (Ensemble X) topology B
In (Ensemble X) topology (Intersection _ A B);

union_stable : I : Type, (Ai : IEnsemble X),
( i : I, In (Ensemble _) topology (Ai i)) →
In (Ensemble X) topology (Infinite_Union X I Ai)
}.

# Separation

Definition separated_space X set topology :=
x y:X,
In _ set xIn _ set y
( Ox Oy, In _ topology OxIn _ topology OyIn _ Ox xIn _ Oy y
z, In _ Ox z In _ Oy z)
→ x = y.

# Sets properties

Lemma intersection_empty_set_absorbing_l :
U:Type, A:Ensemble U,
Intersection U (Empty_set U) A = Empty_set U.
intuition.
Qed.

Lemma intersection_empty_set_absorbing_r :
U:Type, A:Ensemble U,
Intersection U A (Empty_set U) = Empty_set U.
intuition.
Qed.

Lemma intersection_idempotent :
U:Type, A:Ensemble U,
Intersection U A A = A.
intros U A.
apply Extensionality_Ensembles.
unfold Same_set; split; intuition.
Qed.

# Infinite_Union Properties

Lemma subsets_stable_by_Infinite_Union :
(U : Type) (I : Type) (Ai : IEnsemble U) (B : Ensemble U),
( i:I, Included U (Ai i) B) →
Included U (Infinite_Union U I Ai) B.
intros U I Ai B HAi x HIU.
destruct HIU.
elim H; intros i HxAi.
apply (HAi i); assumption.
Qed.

Lemma Infinite_Union_absorbs_subset :
(U : Type) (I : Type) (Ai : IEnsemble U) (B : Ensemble U),
( i:I, Included U B (Ai i)) →
Included U B (Infinite_Union U I Ai).
intros U I Ai B HAi.
elim HAi.
intros i HIi x HxB.
apply Infinite_Union_intro; i.
apply HIi; assumption.
Qed.

Lemma effective_empty : (U:Type) (A:Ensemble U),
( x:U, ¬ In U A x) → A = Empty_set U.
intros U A Nox.
apply Extensionality_Ensembles.
split.

intros x HxA.
apply False_ind.
apply (Nox x); assumption.

intros x Hxnowhere.
induction Hxnowhere.
Qed.

# Trivial topology

Section Trivial_Topology.

Variable U : Type.
Variable set : Ensemble U.

Definition trivial := (Couple (Ensemble U) (Empty_set U) set).

Definition open e := In (Ensemble U) trivial e.

Fact trivial_open_empty_set : open (Empty_set U).
apply Couple_l.
Qed.

Fact trivial_open_full_set : open set.
apply Couple_r.
Qed.

Fact trivial_intersection_stable : A B : Ensemble U,
open Aopen Bopen (Intersection U A B).
intros A B OA OB.
induction OA.
rewrite intersection_empty_set_absorbing_l.
apply Couple_l.
induction OB.
rewrite intersection_empty_set_absorbing_r.
apply Couple_l.
rewrite intersection_idempotent.
apply Couple_r.
Qed.

Lemma open_included_in_set : A, open AIncluded U A set.
intros A OA.
destruct OA; intuition.
Qed.

Require Import ClassicalFacts.

Lemma disjonction_exists : excluded_middle (X:Type) (P:XProp),
( x:X, P x) ( x:X, ¬ P x).
intros EM X P.
elim (EM ( x, P x)).
left; assumption.
right.
intros x Px.
apply H.
x; assumption.
Qed.

Fact trivial_union_stable : excluded_middle
(I:Type) (Ai:IEnsemble U),
( i : I, open (Ai i)) → open (Infinite_Union U I Ai).

intros EM I Ai OAi.
assert (DISJ :
( x : U, In U (Infinite_Union U I Ai) x)
( x : U, ¬ In U (Infinite_Union U I Ai) x) ).
apply (disjonction_exists EM).

elim DISJ; clear DISJ.
intros Hexists; elim Hexists; intros x Hx.
assert ( i : _, In U (Ai i) x) as Geti.
inversion Hx; assumption.

elim Geti; intros i HxAi.
assert (Ai i = set).
assert (Ai i = set Ai i = Empty_set U) as HAi.
assert (open (Ai i)).
apply OAi.

inversion H.
right; reflexivity.

left; reflexivity.

elim HAi.
trivial.

intro Hinv; rewrite Hinv in HxAi; inversion HxAi.

assert (EqUnion : Infinite_Union U I Ai = set).
apply Extensionality_Ensembles.
split.
apply subsets_stable_by_Infinite_Union.
intros i0.
apply open_included_in_set.
apply OAi.

apply (Infinite_Union_absorbs_subset U I Ai).
i; rewrite H in |- *; intuition.

rewrite EqUnion in |- ×.
apply Couple_r.

intros Hfn.
apply (effective_empty U (Infinite_Union U I Ai)) in Hfn.
rewrite Hfn in |- ×.
constructor.
Qed.

Parameter EM : excluded_middle.

Instance trivial_topology : Topological_Space U set trivial := {
open_empty_set := trivial_open_empty_set;
open_full_set := trivial_open_full_set;
intersection_stable := trivial_intersection_stable;
union_stable := (trivial_union_stable EM)
}.
End Trivial_Topology.

# Discrete topology

Section Discrete_Topology.

Variable U : Type.
Variable set : Ensemble U.

Definition discrete := Power_set U set.

Definition part e := In (Ensemble U) discrete e.

Fact discrete_open_empty_set : part (Empty_set U).
apply Definition_of_Power_set.
intuition.
Qed.

Fact discrete_open_full_set : part set.
apply Definition_of_Power_set.
intuition.
Qed.

Fact discrete_intersection_stable : A B : Ensemble U,
part Apart Bpart (Intersection U A B).
intros A B pA _.
apply Definition_of_Power_set.
intros x xI.
destruct xI; clear H0.
destruct pA.
apply H0.
assumption.
Qed.

Fact discrete_union_stable : I : Type, Ai : IEnsemble U,
( i : I, part (Ai i)) → part (Infinite_Union U I Ai).
intros I Ai pAi.

apply Definition_of_Power_set.
apply subsets_stable_by_Infinite_Union.
intros i x HxAi.
assert (Included U (Ai i) set).
assert (part (Ai i)).
apply pAi.
destruct H; assumption.

unfold Included in × |- .
apply H; assumption.
Qed.

Instance discrete_topology : Topological_Space U set discrete := {
open_empty_set := discrete_open_empty_set;
open_full_set := discrete_open_full_set;
intersection_stable := discrete_intersection_stable;
union_stable := discrete_union_stable
}.
End Discrete_Topology.