addHaar_closedBall_eq_addHaar_ball

English

There exists equality μ(closedBall x r) = μ(ball x r) for Haar measure μ when E is nontrivial.

Русский

Для ненулевого пространства E справедливо μ(closedBall x r) = μ(ball x r) для меры Хаара μ.

LaTeX

$$$\mu(closedBall(x, r)) = \mu(ball(x, r))$$$

Lean4

theorem addHaar_closedBall_eq_addHaar_ball [Nontrivial E] (x : E) (r : ℝ) : μ (closedBall x r) = μ (ball x r) :=
  by
  by_cases h : r < 0
  · rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]
  push_neg at h
  rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

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