English
Let I be an index set and l_i (i ∈ I) a family of filters on α. Suppose S ⊆ I is finite and S.PairwiseDisjoint l, and for every i ∈ I, (l_i)HasBasis(p_i, s_i). Then there exists ind : ∀ i, ι i such that ∀ i, p_i(ind i) and S.PairwiseDisjoint (λ i. s_i(ind i)).
Русский
Пусть I — множество индексов и для каждого i∈I дано фильтр l_i на α. Пусть S⊆I конечно и S PairwiseDisjoint l, и для каждого i ∈ I л_i имеет базис (p_i, s_i). Тогда существует выбор ind: ∀ i, ι i such that ∀ i, p_i(ind i) и S попарно непересекаются наборы s_i(ind i).
LaTeX
$$$\exists ind : \forall i, ι i,\ (\forall i, p i (ind i)) \land S.\ PairwiseDisjoint (\lambda i. s i (ind i)).$$$
Lean4
theorem _root_.Set.PairwiseDisjoint.exists_mem_filter_basis {I : Type*} {l : I → Filter α} {ι : I → Sort*}
{p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} {S : Set I} (hd : S.PairwiseDisjoint l) (hS : S.Finite)
(h : ∀ i, (l i).HasBasis (p i) (s i)) :
∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i) :=
by
rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
exact ⟨ind, hp, hd.mono ht⟩
