addHaar_real_closedBall_eq_addHaar_real_ball

English

Let μ be a Haar measure on E. Then μ(sphere x r) = 0 for any r ≠ 0.

Русский

Пусть μ — мера Хаара на E. Тогда μ(sphere x r) = 0 для любого r ≠ 0.

LaTeX

$$$\mu(sphere(x, r)) = 0 \quad \text{если } r \neq 0$$$

Lean4

theorem addHaar_real_closedBall_eq_addHaar_real_ball [Nontrivial E] (x : E) (r : ℝ) :
    μ.real (closedBall x r) = μ.real (ball x r) := by simp [measureReal_def, addHaar_closedBall_eq_addHaar_ball μ x r]

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