addHaar_real_closedBall — Mathlib

English

For Nontrivial E and r ≥ 0, μ.real(closedBall x r) = r^finrank E · μ.real(closedBall 0 1).

Русский

Для ненулевого E и r ≥ 0: μ.real(closedBall x r) = r^finrank E · μ.real(closedBall(0,1)).

LaTeX

$$$\mu_{\mathbb{R}}(\overline{B}(x, r)) = r^{\mathrm{finrank}\,\mathbb{R} E} \cdot \mu_{\mathbb{R}}(\overline{B}(0, 1))$$$

Lean4

theorem addHaar_real_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (ball 0 1) := by
  simp [addHaar_real_closedBall' μ x hr, measureReal_def, addHaar_unitClosedBall_eq_addHaar_unitBall]

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