Theorems · Definition · measure theory

MeasureTheory.QuotientMeasureEqMeasurePreimage.casesOn

{G : Type u_1} →
  {α : Type u_3} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        [inst_2 : MeasurableSpace α] →
          {ν : MeasureTheory.Measure α} →
            {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} →
              {motive : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ → Sort u} →
                (t : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ) →
                  ((projection_respects_measure' :
                        ∀ (t : Set α),
                          MeasureTheory.IsFundamentalDomain G t ν →
                            μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.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

GroupMulActionMeasurableSpace