Theorems · Theorem · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient

∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  [i : MeasureTheory.SigmaFinite ν] [i' : MeasureTheory.HasAddFundamentalDomain G α ν]
  (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ], MeasureTheory.SigmaFinite μ

If a measure μ on a quotient satisfies AddQuotientMeasureEqMeasurePreimage with respect to a sigma-finite measure ν, then it is itself SigmaFinite.

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionMeasurableSpaceMeasureTheory.VAddInvariantMeasureCountableMeasurableConstVAddMeasureTheory.SigmaFiniteMeasureTheory.HasAddFundamentalDomainMeasureTheory.AddQuotientMeasureEqMeasurePreimage