proposition: Lemma metric_space_fun_continuity_converse: forall (X Y:TopologicalSpace) (f:X->Y) (x:X) (dX:X -> X -> R) (dY:Y -> Y -> R), metrizes X dX -> metrizes Y dY -> continuous_at f x -> forall eps:R, eps > 0 -> exists delta:R, delta > 0 /\ forall x':X, dX x x' < delta -> dY (f x) (f x') < eps.
proof: Proof. intros. destruct (H x). destruct (H0 (f x)). assert (neighborhood (open_ball dY (f x) eps) (f x)). { apply open_neighborhood_is_neighborhood. apply open_neighborhood_basis_elements0. now constructor. } apply H1 in H3. destruct H3 as [U]. destruct H3. destruct (open_neighborhood_basis_cond U H3) as [V]. destruct H5. destruct H5 as [delta]. exists delta. split; trivial. intros. assert (In (inverse_image f (open_ball dY (f x) eps)) x'). { apply H4, H6. now constructor. } destruct H8. now destruct H8. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)