Theorems · Theorem · general topology

Filter.hasBasis_biInf_principal

∀ {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β},
  DirectedOn (s ⁻¹'o fun x1 x2 => x1 ⊇ x2) S →
    S.Nonempty → (⨅ i ∈ S, Filter.principal (s i)).HasBasis (fun i => i ∈ S) s

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

5 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Quot.sound