measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage

English

The Haar measure on a product of two spaces equals the product of the Haar measures on each factor.

Русский

Мера Хаара на произведении пространств равна произведению мер Хаара на каждом факторе.

LaTeX

$$$(v.prod w).addHaar = v.addHaar.prod w.addHaar$$$

Lean4

/-- Given a subgroup `Γ` of a topological group `G` with measure `ν`, and a measure 'μ' on the
  quotient `G ⧸ Γ` satisfying `QuotientMeasureEqMeasurePreimage`, the restriction
  of `ν` to a fundamental domain is measure-preserving with respect to `μ`. -/
@[to_additive]
theorem measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage {𝓕 : Set G}
    (h𝓕 : IsFundamentalDomain Γ.op 𝓕 ν) (μ : Measure (G ⧸ Γ)) [QuotientMeasureEqMeasurePreimage ν μ] :
    MeasurePreserving (@QuotientGroup.mk G _ Γ) (ν.restrict 𝓕) μ :=
  h𝓕.measurePreserving_quotient_mk μ

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