Theorems · Theorem · measure theory

isFoelner_iff

∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X),
  IsFoelner G μ l F ↔
    (∀ᶠ (i : ι) in l, MeasurableSet (F i)) ∧
      (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) ∧
        (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) ∧
          ∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)

Defined in

Mathlib.MeasureTheory.Group.FoelnerFilter

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceGroupMulAction