measure_closedBall_pos_iff — Mathlib

English

For metric spaces with NoAtoms μ, μ(closedBall x r) > 0 iff r > 0.

Русский

В метрическом пространстве с NoAtoms μ, μ(закрытого шара) > 0 тогда и только тогда, когда r > 0.

LaTeX

$$$\\forall x,\\; 0 < r \\Rightarrow (μ(\\mathrm{closedBall} x r) > 0) \\iff r > 0.$$$

Lean4

@[simp]
theorem measure_closedBall_pos_iff {X : Type*} [MetricSpace X] {m : MeasurableSpace X} (μ : Measure X)
    [IsOpenPosMeasure μ] [NoAtoms μ] {x : X} {r : ℝ} : 0 < μ (closedBall x r) ↔ 0 < r :=
  by
  refine ⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩
  contrapose! h
  rw [(subsingleton_closedBall x h).measure_zero μ]

Похожие утверждения