proposition: Lemma closed_ball_radius_zero X d (x0 : X) : metric d -> closed_ball d x0 0 = Singleton x0.
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - destruct H0. apply Singleton_intro. apply (metric_strict _ _ H). apply Rle_antisym; try assumption. pose proof (metric_nonneg _ _ H x0 x). lra. - constructor. destruct H0. rewrite metric_zero; auto; lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)