Theorems · Inductive type · measure theory

MeasureTheory.IsAddFundamentalDomain

(G : Type u_1) →
  {α : Type u_2} →
    [Zero G] →
      [VAdd G α] →
        [inst : MeasurableSpace α] →
          Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1 → Prop

A measurable set s is a fundamental domain for an additive action of an additive group G on a measurable space α with respect to a measure μ if the sets g +ᵥ s, g : G, are pairwise a.e. disjoint and cover the whole space.

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

88 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

ZeroVAddMeasurableSpace