proposition: Lemma metric_closed_ball_In X (d : X -> X -> R) : metric d -> forall x r, 0 <= r <-> In (closed_ball d x r) x.
proof: Proof. intros. pose proof (metric_zero X d H x). split. - intros. constructor. lra. - intros. destruct H1. lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)