fact: Definition closed_ball (x0 : X) (r : R) : Ensemble X := [x : X | d x0 x <= r].
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)