Theorems · Theorem · general topology

Filter.HasBasis.frequently_iff

∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {q : α → Prop}, (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

16 results in Mathlib

Foundations

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