proposition: Lemma metric_space_closed_ball_closed {X : TopologicalSpace} (d : X -> X -> R) : metrizes X d -> metric d -> forall x r, closed (closed_ball d x r).
proof: Proof. intros. red. apply open_char_neighborhood. intros. exists (open_ball d x0 (d x x0 - r)). split. - split. + apply metric_space_open_ball_open; assumption. + apply metric_open_ball_In; auto. apply NNPP. intros ?. apply H1. constructor. lra. - intros ? ?. destruct H2. intros ?. destruct H3. pose proof (triangle_inequality X d H0 x x1 x0). rewrite (metric_sym X d H0 x1 x0) in H4. lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)