Theorems · Theorem · general topology

Filter.HasBasis.forall_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 s → P t) → ((∀ s ∈ l, P s) ↔ ∀ (i : ι), p i → P (s i))

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

15 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms