Theorems · Definition · measure theory

IsFoelner.casesOn

{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} →
                  {motive : IsFoelner G μ l F → Sort u} →
                    (t : IsFoelner G μ l F) →
                      ((eventually_measurableSet : ∀ᶠ (i : ι) in l, MeasurableSet (F i)) →
                          (eventually_meas_ne_zero : ∀ᶠ (i : ι) in l, μ (F i) ≠ 0) →
                            (eventually_meas_ne_top : ∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) →
                              (tendsto_meas_smul_symmDiff :
                                  ∀ (g : G),
                                    Filter.Tendsto (fun i => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)) →
                                motive ⋯) →
                        motive t

Defined in

Mathlib.MeasureTheory.Group.FoelnerFilter

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceGroupMulAction