volume_preimage_mul_right — Mathlib

English

If M is invertible, the Lebesgue volume pushed forward by the linear map M equals ENNReal.ofReal(|det M|⁻¹) times the original volume.

Русский

Если матрица M обратима, то образ объёма Лебега под линейным отображением M равен ENNReal.ofReal(|det M|⁻¹) умноженному на исходный объём.

LaTeX

$$$$ \\mathrm{map} (\\text{toLin'}~M) ~\\mathrm{volume} = \\mathrm{ENNReal.ofReal}(|\\det M|^{-1}) \\cdot \\mathrm{volume}. $$$$

Lean4

@[simp]
theorem volume_preimage_mul_right {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.mulRight₀ a h).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs a⁻¹) * volume s := by rw [map_volume_mul_right h]; rfl

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