English
From a pairwise disjoint family of Finite indexed filters, there exists a family of sets s i with s i ∈ l i and pairwise disjoint on s.
Русский
Из пары взаимоисключающих семейства фильтров с конечной индексной множеством существует семейство множеств s_i, где s_i ∈ l_i и пары s_i попарно дизъюнкты.
LaTeX
$$$ (\mathrm{Pairwise}\; \mathrm{Disjoint}\ on\ l)\ \Rightarrow \ \exists s: ι \to Set α,\ (\forall i, s(i) \in l(i)) \land \mathrm{Pairwise} (Disjoint on s) $$$
Lean4
theorem _root_.Pairwise.exists_mem_filter_of_disjoint {ι : Type*} [Finite ι] {l : ι → Filter α}
(hd : Pairwise (Disjoint on l)) : ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ Pairwise (Disjoint on s) :=
by
have : Pairwise fun i j => ∃ (s : { s // s ∈ l i }) (t : { t // t ∈ l j }), Disjoint s.1 t.1 := by
simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd
choose! s t hst using this
refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
(hst hij).mono ((iInter_subset _ j).trans inter_subset_left) ((iInter_subset _ i).trans inter_subset_right)]
