Theorems · Theorem · measure theory

MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient

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

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

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMeasurableSpaceTopologicalSpaceIsTopologicalGroupBorelSpacePolishSpaceSubgroup.NormalT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.HasFundamentalDomainMeasureTheory.QuotientMeasureEqMeasurePreimage