Theorems · Theorem · measure theory

MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient

∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : Subgroup G}
  {μ : MeasureTheory.Measure (G ⧸ Γ)} [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] [inst_3 : TopologicalSpace G]
  [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)]
  [ν.IsMulLeftInvariant] [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.SMulInvariantMeasure G (G ⧸ Γ) μ

If μ satisfies QuotientMeasureEqMeasurePreimage relative to a both left- and right- invariant measure ν on G, then it is a G invariant measure on G ⧸ Γ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMeasurableSpaceMeasureTheory.QuotientMeasureEqMeasurePreimageTopologicalSpaceIsTopologicalGroupBorelSpacePolishSpaceT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.HasFundamentalDomain