proposition: Lemma metric_open_ball_radius_nonpositive X d : @metric X d -> forall x r, r <= 0 -> open_ball d x r = Empty_set.
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros; try contradiction. destruct H1. pose proof (metric_nonneg X d H x x0). lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)