volume_preimage_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : Set ℝ) :
    volume ((a * ·) ⁻¹' s) = ENNReal.ofReal (abs a⁻¹) * volume s :=
  calc
    volume ((a * ·) ⁻¹' s) = Measure.map (a * ·) volume s :=
      ((Homeomorph.mulLeft₀ a h).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs a⁻¹) * volume s := by rw [map_volume_mul_left h]; rfl

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