smul_map_volume_mul_right — Mathlib

English

For a ≠ 0, volume ((· · a)⁻¹' s) = ENNReal.ofReal(|a⁻¹|) · volume s.

Русский

Для a ≠ 0, предобраз под умножением справа имеет объём ENNReal.ofReal(|a⁻¹|) · volume s.

LaTeX

$$$$ \\mathrm{volume}((\\cdot \\cdot a)^{-1} s) = \\mathrm{ENNReal.ofReal}(|a^{-1}|) \\cdot \\mathrm{volume}(s). $$$$

Lean4

theorem smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) : ENNReal.ofReal |a| • Measure.map (· * a) volume = volume := by
  simpa only [mul_comm] using Real.smul_map_volume_mul_left h

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