English
From a pairwise disjoint family of filters indexed by a finite set, there exists a family of sets s_i with s_i ∈ l_i and the family s_i is pairwise disjoint.
Русский
Из пары взаимоисключающих семейств фильтров индексируемых конечным множеством существует семейство множеств s_i с s_i ∈ l_i, и множество s_i попарно несовместны.
LaTeX
$$$ \text{Set}.PairwiseDisjoint.exists_mem_filter \ (hd)\ (ht) : \exists s : ι \to Set α, (\forall i, s i \in l i) ∧ t.PairwiseDisjoint s $$$
Lean4
@[simp]
theorem iInf_principal_finset {ι : Type w} (s : Finset ι) (f : ι → Set α) : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i) := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
