Theorems · Inductive type · measure theory

MeasureTheory.QuotientMeasureEqMeasurePreimage

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

Measures ν on α and μ on the Quotient of α mod G satisfy QuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable subset U of the quotient, μ U = ν ((π ⁻¹' 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

GroupMulActionMeasurableSpace