Theorems · Theorem · measure theory

IsFoelner.tendsto_meas_smul_symmDiff

∀ {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 → ∀ (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: 3 results in Mathlib
Foundations: Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace Group MulAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
Filterstatement and proof · cited by 8,121
Groupstatement and proof · cited by 6,238
nhdsstatement · cited by 5,554
Filter.Tendstostatement · cited by 3,814
MulActionstatement and proof · cited by 1,294
Set.smulSetstatement · cited by 608
symmDiffstatement · cited by 236

Cited by3

Results whose statement or proof uses this declaration.

IsFoelner.tendsto_meas_smul_symmDiff_smulproof · cited by 1
IsFoelner.monoproof · cited by 1
IsFoelner.comp_tendstoproof · cited by 0