Theorems · Theorem · general topology

Filter.HasBasis.iInf

∀ {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop}
  {s : (i : ι) → ι' i → Set α},
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) →
    (⨅ i, l i).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun If => ⋂ i, s (↑i) (If.snd i)

Defined in

Mathlib.Order.Filter.Bases.Finite

Cited by

3 results in Mathlib

Foundations

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