proposition: Lemma metric_space_open_ball_open : forall (X:TopologicalSpace) (d:X -> X -> R), metrizes X d -> metric d -> forall x r, open (open_ball d x r).
proof: Proof. intros. specialize (H x). destruct (classic (r > 0)). - assert (In (metric_topology_neighborhood_basis d x) (open_ball d x r)). { constructor. assumption. } apply H in H2. destruct H2. assumption. - rewrite metric_open_ball_radius_nonpositive; auto with topology; lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)