proposition: Lemma metric_space_fun_continuity: forall (X Y:TopologicalSpace) (f:X->Y) (x:X) (dX:X -> X -> R) (dY:Y -> Y -> R), metrizes X dX -> metrizes Y dY -> (forall eps:R, eps > 0 -> exists delta:R, delta > 0 /\ forall x':X, dX x x' < delta -> dY (f x) (f x') < eps) -> continuous_at f x.
proof: Proof. intros. destruct (H x). destruct (H0 (f x)). red; intros. destruct H2 as [V']. destruct H2. destruct (open_neighborhood_basis_cond0 V' H2). destruct H4. destruct H4 as [eps]. destruct (H1 eps H4) as [delta []]. exists (open_ball dX x delta). split. - apply open_neighborhood_basis_elements. now constructor. - intros x' ?. destruct H8. constructor. apply H3, H5. constructor. now apply H7. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)