addHaar_image_continuousLinearEquiv

English

For a linear equivalence f, the preimage scales by |det f|: μ(f^{-1}(s)) = |det f| μ(s).

Русский

Для линейного эквивалентного отображения f предел предобраза масштабируется на |det f|: μ(f^{-1}(S)) = |det f| μ(S).

LaTeX

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

Lean4

/-- The image of a set `s` under a continuous linear equiv `f` has measure
equal to `μ s` times the absolute value of the determinant of `f`. -/
@[simp]
theorem addHaar_image_continuousLinearEquiv (f : E ≃L[ℝ] E) (s : Set E) :
    μ (f '' s) = ENNReal.ofReal |LinearMap.det (f : E →ₗ[ℝ] E)| * μ s :=
  μ.addHaar_image_linearMap (f : E →ₗ[ℝ] E) s

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