addHaar_sphere_of_ne_zero — Mathlib

English

If r ≠ 0, then μ(sphere x r) = 0 for Haar measure μ on E.

Русский

Если r ≠ 0, то μ(sphere x r) = 0 для меры Хаара μ на E.

LaTeX

$$$\mu(sphere(x, r)) = 0$$$

Lean4

theorem addHaar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) : μ (sphere x r) = 0 :=
  by
  rcases hr.lt_or_gt with (h | h)
  · simp only [empty_diff, measure_empty, ← closedBall_diff_ball, closedBall_eq_empty.2 h]
  ·
    rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]

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