proposition: Lemma metric_space_net_limit_converse: forall (X:TopologicalSpace) (d:X -> X -> R), metrizes X d -> forall (I:DirectedSet) (x:Net I X) (x0:X), net_limit x x0 -> forall eps:R, eps > 0 -> for large i:DS_set I, d x0 (x i) < eps.
proof: Proof. intros. pose (U:=open_ball d x0 eps). assert (open_neighborhood U x0). { apply H. now constructor. } destruct H2. destruct (H0 U) as [i]; trivial. exists i. intros. now apply H4. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)