Theorems · Definition · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage.recOn

{G : Type u_1} →
  {α : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        [inst_2 : MeasurableSpace α] →
          {ν : MeasureTheory.Measure α} →
            {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} →
              {motive : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ → Sort u} →
                (t : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ) →
                  ((addProjection_respects_measure' :
                        ∀ (t : Set α),
                          MeasureTheory.IsAddFundamentalDomain G t ν →
                            μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)) →
                      motive ⋯) →
                    motive t

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionMeasurableSpace