map_volume_mul_right — Mathlib

English

For a ≠ 0, map (· · a) volume equals ENNReal.ofReal(|a⁻¹|) times volume.

Русский

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

LaTeX

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

Lean4

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

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