proposition: Lemma metric_space_net_cluster_point: forall (X:TopologicalSpace) (d:X -> X -> R), metrizes X d -> forall (I:DirectedSet) (x:Net I X) (x0:X), (forall eps:R, eps > 0 -> exists arbitrarily large i:DS_set I, d x0 (x i) < eps) -> net_cluster_point x x0.
proof: Proof. intros. red. intros. destruct (H x0). destruct (open_neighborhood_basis_cond U) as [? [[]]]. - now split. - red. intros. destruct (H0 r H3 i) as [j []]. exists j; split; trivial. apply H4. now constructor. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)