proposition: Lemma metric_space_net_cluster_point_converse: forall (X:TopologicalSpace) (d:X -> X -> R), metrizes X d -> forall (I:DirectedSet) (x:Net I X) (x0:X), net_cluster_point x x0 -> forall eps:R, eps > 0 -> exists arbitrarily 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. pose proof (H0 U H2 H3). red. intros. destruct (H4 i) as [j []]. exists j. split; trivial. now destruct H6. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)