mulEquivHaarChar_smul_preimage — Mathlib

English

For Haar μ, φ, and any X, mulEquivHaarChar φ · μ(φ^{-1} X) = μ(X).

Русский

Для μ и φ, и множества X: mulEquivHaarChar φ · μ(φ^{-1}(X)) = μ(X).

LaTeX

$$$mulEquivHaarChar(\phi) \cdot μ(φ^{-1} X) = μ(X)$$$

Lean4

@[to_additive addEquivAddHaarChar_smul_preimage]
theorem mulEquivHaarChar_smul_preimage (μ : Measure G) [IsHaarMeasure μ] [Regular μ] {X : Set G} (φ : G ≃ₜ* G) :
    mulEquivHaarChar φ • μ (φ ⁻¹' X) = μ X :=
  by
  nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
  simp only [smul_apply, nnreal_smul_coe_apply]
  exact congr_arg _ <| (MeasurableEquiv.map_apply φ.toMeasurableEquiv X).symm

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