# Topological space

Require Import Reals.
Require Import Ensembles.
Require Import Topology.
Require Import Fourier.

# Metric Space

Class Metric_Space
(X : Type)
(d : XXR)
:= {
metric_pos : x y, (0 d x y)%R;
metric_sym : x y, d x y = d y x;
metric_refl : x y, (d x y = 0 x = y)%R;
metric_tri : x y z, (d x y d x z + d z y)%R
}.

# Open sets

Section Open_sets.
Variable X : Type.
Variable d : XXR.

Open Scope R_scope.

Definition metric_open W: Prop :=
x, In _ W x eps:R, 0 < eps
y, d x y < epsIn _ W y.

End Open_sets.

# Balls

Section Balls.
Variable X : Type.
Variable d : XXR.
Variable E : Metric_Space X d.

Inductive open_ball c r (rpos : (0 < r)%R) : Ensemble X :=
open_ball_intro : x, (d x c < r)%RIn _ (open_ball c r rpos) x.

Inductive closed_ball c r (rpos : (0 < r)%R) : Ensemble X :=
closed_ball_intro : x, (d x c r)%RIn _ (closed_ball c r rpos) x.

Lemma open_ball_is_open : c r rpos, metric_open X d (open_ball c r rpos).
Proof.
intros c r rpos x Hx.
destruct Hx as [x Hxc].
(r - d x c)%R; split.
apply Rlt_Rminus; auto.

intros y Hxy.
constructor.
eapply Rle_lt_trans.
apply (metric_tri _ _ x).

rewrite (metric_sym y x); fourier.
Qed.
End Balls.

# A metric space defines a topology

Section Metric_topology.
Variable X : Type.
Variable d : XXR.

Fact metric_open_empty_set : metric_open X d (Empty_set _).
intros x H.
inversion H.
Qed.

Fact metric_open_full_set : metric_open X d (Full_set _).
intros x _.
1%R.
split. intuition.
intros y _.
constructor.
Qed.

Fact metric_intersection_stable : A B : Ensemble _,
metric_open X d Ametric_open X d B
metric_open X d (Intersection _ A B).
intros A B OA OB.
intros x [y yA yB].
elim (OA y). intros epsa [epsapos opena].
elim (OB y). intros epsb [epsbpos openb].
(Rmin epsa epsb).
split.
apply Rmin_Rgt_r.
split; assumption.
intros x' inx'.
apply Rmin_Rgt_l in inx' as [ax' bx'].
apply Intersection_intro;
[apply opena | apply openb];
apply Rgt_lt; assumption.
assumption.
assumption.
Qed.

Fact metric_union_stable : I : Type, Ai : IEnsemble _,
( i : I, metric_open X d (Ai i)) → metric_open X d (Infinite_Union _ I Ai).
intros I Ai openAi.
intros x xinU.
induction xinU.
elim H. intros i inxAi.
elim (openAi i x).
intros eps [epspos B].
eps.
split.
exact epspos.
intros y yinB.
. i.
apply (B _ yinB).
assumption.
Qed.

Instance metric_space_topological : Topological_Space _ (Full_set _) (metric_open X d) := {
open_empty_set := metric_open_empty_set;
open_full_set := metric_open_full_set;
intersection_stable := metric_intersection_stable;
union_stable := metric_union_stable
}.
End Metric_topology.

# A metric space is separated

Lemma metric_space_is_separated : X d (MX : Metric_Space X d),
separated_space X (Full_set X) (metric_open X d).
Proof.
intros X d MX x y _ _ H.
apply (proj1 (metric_refl _ _)).
destruct (Rtotal_order (d x y) 0%R) as [|[|]]; auto.
apply RIneq.Rle_not_lt in H0.
apply metric_pos.
pose (d x y / 2)%R as r.
assert (rpos : 0 < r).
unfold r; fourier.
pose (fun copen_ball X d c r rpos) as ball.
assert (centerinball : x, ball x x).
constructor.
rewrite (proj2 (metric_refl _ _)); auto.
destruct (H (ball x) (ball y)
(open_ball_is_open _ _ _ _ _ _)
(open_ball_is_open _ _ _ _ _ _)
(centerinball _)
(centerinball _)) as [z []].
destruct H1 as [z H1].
destruct H2 as [z H2].
unfold r in ×.
assert (d x y < d x y).
apply Rle_lt_trans with (d z x + d z y).
rewrite metric_sym with z x; apply metric_tri.

replace (d x y) with (d x y / 2 + d x y / 2) by field.
apply Rplus_lt_compat; auto.
apply Rlt_irrefl in H3.