English
If a finite set t of indices has pairwise disjoint l_i, then there exists s: ι → Set α with s i ∈ l i and t.PairwiseDisjoint s.
Русский
Если конечное множество индексов t имеет попарно несовместные l_i, то существует s: ι → Set α с s i ∈ l i и t.PairwiseDisjoint s.
LaTeX
$$$ t.PairwiseDisjoint l \to\ t.Finite \to \exists s : ι \to Set α, (\forall i, s i \in l i) ∧ t.PairwiseDisjoint s $$$
Lean4
theorem _root_.Set.PairwiseDisjoint.exists_mem_filter {ι : Type*} {l : ι → Filter α} {t : Set ι}
(hd : t.PairwiseDisjoint l) (ht : t.Finite) : ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ t.PairwiseDisjoint s :=
by
haveI := ht.to_subtype
rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩
lift s to (i : t) → { s // s ∈ l i } using hsl
rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩
exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩
