Theorems · Inductive type · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage

{G : Type u_1} →
  {α : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        [inst_2 : MeasurableSpace α] →
          autoParam (MeasureTheory.Measure α) MeasureTheory.AddQuotientMeasureEqMeasurePreimage._auto_1 →
            MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)) → Prop

A measure μ on the AddQuotient of α mod G satisfies AddQuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable subset U of the quotient, μ U = volume ((π ⁻¹' U) ∩ t).

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

19 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionMeasurableSpace