Theorems · Theorem · general topology

Pairwise.exists_mem_filter_basis_of_disjoint

∀ {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {p : (i : I) → ι i → Prop}
  {s : (i : I) → ι i → Set α},
  Pairwise (Function.onFun Disjoint l) →
    (∀ (i : I), (l i).HasBasis (p i) (s i)) →
      ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Function.onFun Disjoint fun i => s i (ind i))

Defined in

Mathlib.Order.Filter.Bases.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite