map_volume_mul_left — Mathlib

English

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

Русский

Для a ≠ 0 отображение объема равно ENNReal.ofReal |a⁻¹| умножению объема.

LaTeX

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

Lean4

theorem map_volume_mul_left {a : ℝ} (h : a ≠ 0) : Measure.map (a * ·) volume = ENNReal.ofReal |a⁻¹| • volume := by
  conv_rhs =>
    rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ h,
      abs_one, ENNReal.ofReal_one, one_smul]

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