Theorems · Theorem · general topology

Filter.HasBasis.frequently_smallSets

∀ {α : Type u_4} {ι : Sort u_5} {p : ι → Prop} {l : Filter α} {s : ι → Set α} {q : Set α → Prop} {hl : l.HasBasis p s},
  (∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t) → ((∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i))

Defined in

Mathlib.Order.Filter.SmallSets

Cited by

5 results in Mathlib

Foundations

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