addHaar_preimage_linearEquiv — Mathlib

English

For a linear equivalence f: E ≃ E, μ(f^{-1}(s)) = |det f| μ(s).

Русский

Для линейного эквивалента f: E ≃ E выполняется μ(f^{-1}(S)) = |det f| μ(S).

LaTeX

$$$\\mu(f^{-1}(S)) = |\\det f| \\mu(S)$$$

Lean4

/-- The preimage of a set `s` under a linear equiv `f` has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
@[simp]
theorem addHaar_preimage_linearEquiv (f : E ≃ₗ[ℝ] E) (s : Set E) :
    μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det (f.symm : E →ₗ[ℝ] E)| * μ s :=
  by
  have A : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0 := (LinearEquiv.isUnit_det' f).ne_zero
  convert addHaar_preimage_linearMap μ A s
  simp only [LinearEquiv.det_coe_symm]

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