# Library Coqtail.Topology.TContinuity

Require Import Reals.
Require Import Ensembles.
Require Import Topology.
Require Import Functions.
Require Import Metrics.
Require Import TFunctions.

Definition Topological_Continuity
(U:Type) (V:Type)
(A:Ensemble U) (B:Ensemble V)
(TA:Ensemble (Ensemble U)) (TB:Ensemble (Ensemble V))
(TopA : Topological_Space U A TA) (TopB : Topological_Space V B TB)
(f : UV) : Prop := function U V A B f
OB, In _ TB OBIn _ TA (Intersection _ (Preimage _ _ OB f) A).

Open Scope R_scope.

Definition Metric_Continuity_Pt
(U:Type) (V:Type)
(dU : UUR) (dV : VVR)
(MU : Metric_Space U dU) (MV : Metric_Space V dV)
(f : UV) (a : U) : Prop :=
eps:R, 0<eps
delta:R, 0<delta
a',
dU a a' < delta
dV (f a) (f a') < eps.

Definition Metric_Continuity
(U:Type) (V:Type)
(dU : UUR) (dV : VVR)
(MU : Metric_Space U dU) (MV : Metric_Space V dV)
(f : UV) : Prop :=
a, Metric_Continuity_Pt U V dU dV MU MV f a.

Lemma metric_continuity_is_topological :
(U:Type) (V:Type)
(dU : UUR) (dV : VVR)
(MU : Metric_Space U dU) (MV : Metric_Space V dV)
(f : UV),
Metric_Continuity U V dU dV MU MV f
Topological_Continuity U V (Full_set U) (Full_set V)
(metric_open _ dU) (metric_open _ dV)
(metric_space_topological _ _) (metric_space_topological _ _)
f.
Proof.
intros U V dU dV MU MV f HMC Hfun O openO x Hx.
assert (Intersection U (Preimage U V O f) (Full_set U) = Preimage U V O f).
apply Extensionality_Ensembles; split; auto with sets.
intros t Ht; split; auto; constructor.
rewrite H in Hx; rewrite H; clear H.
destruct openO with (f x) as [e [epos He]]; destruct Hx; subst; auto.
destruct (HMC x e epos) as [d [dpos Hd]].
d.
split; auto.
intros y Hxy.
pose proof He (f y) (Hd y Hxy).
econstructor; auto; auto.
Qed.