addHaar_closedBall_center — Mathlib

English

The Haar measure of a closed ball is invariant under translation; μ(closedBall(x,r)) = μ(closedBall(0,r)).

Русский

Гааровa мера закрытого шара инвариантна относительно переноса: μ(closedBall(x,r)) = μ(closedBall(0,r)).

LaTeX

$$μ(closedBall(x,r)) = μ(closedBall(0,r))$$

Lean4

theorem addHaar_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E)
    [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (closedBall x r) = μ (closedBall (0 : E) r) :=
  by
  have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall]
  rw [this, measure_preimage_add]

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