Theorems · Theorem · general topology

Set.PairwiseDisjoint.exists_mem_filter_basis

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

Defined in

Mathlib.Order.Filter.Bases.Finite

Cited by

1 results in Mathlib

Foundations

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