addHaar_preimage_continuousLinearMap

English

If f is a linear equivalence, then μ(f^{-1}(s)) = |det f| μ(s) with appropriate normalization, equivalently μ(f^{-1}(s)) = |det f^{-1}| μ(s).

Русский

Если f — линейное эквивалентное отображение, то μ(f^{-1}(S)) = |det f| μ(S) (или эквивалентно = |det f^{-1}| μ(S)).

LaTeX

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

Lean4

/-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
@[simp]
theorem addHaar_preimage_continuousLinearMap {f : E →L[ℝ] E} (hf : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0) (s : Set E) :
    μ (f ⁻¹' s) = ENNReal.ofReal (abs (LinearMap.det (f : E →ₗ[ℝ] E))⁻¹) * μ s :=
  addHaar_preimage_linearMap μ hf s

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