theorem IsFoelner.eventually_measureReal_ne_zero {G : Type u_1} {X : Type u_2} {ι : Type u_3} [MeasurableSpace X] [Group G] [MulAction G X] {μ : MeasureTheory.Measure X} {l : Filter ι} {F : ι → Set X} (hF : IsFoelner G μ l F) : ∀ᶠ (i : ι) in l, μ.real (F i) ≠ 0