Theorems · Theorem · general topology

Filter.HasBasis.exists_iff

∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {P : Set α → Prop}, (∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s) → ((∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i))

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

12 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms