map_hausdorffMeasure — Mathlib

English

The pushforward map by an isometry coincides with the restriction to the range of the measure.

Русский

Перемещение меры по изометрии совпадает с ограничением на диапазон образа.

LaTeX

$$$\text{map } f\; μ_H^{d} = μ_H^{d}\restrict(\mathrm{range}(f))$$$

Lean4

theorem map_hausdorffMeasure (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) :
    Measure.map f μH[d] = μH[d].restrict (range f) := by
  ext1 s hs
  rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs, hf.hausdorffMeasure_preimage hd]

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