Theorems · Theorem · measure theory

MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one

∀ {G : Type u_5} {α : Type u_6} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
    (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g • s)

Defined in

Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction