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 : U→V) : Prop := function U V A B f →
  ∀ OB, In _ TB OB → In _ TA (Intersection _ (Preimage _ _ OB f) A).

Open Scope R_scope.

Definition Metric_Continuity_Pt
  (U:Type) (V:Type)
  (dU : U → U → R) (dV : V → V → R)
  (MU : Metric_Space U dU) (MV : Metric_Space V dV)
  (f : U→V) (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 : U → U → R) (dV : V → V → R)
  (MU : Metric_Space U dU) (MV : Metric_Space V dV)
  (f : U→V) : Prop :=
    ∀ a, Metric_Continuity_Pt U V dU dV MU MV f a.

Lemma metric_continuity_is_topological : ∀
  (U:Type) (V:Type)
  (dU : U → U → R) (dV : V → V → R)
  (MU : Metric_Space U dU) (MV : Metric_Space V dV)
  (f : U→V),
    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.