English
Let (l_i) be a family of filters on the sets α_i and let (s_i) be a family of subsets with s_i ∈ l_i for every i. If all but finitely many s_i equal the whole space α_i, then the indexed product set { a ∈ ∏ i α_i | ∀ i, a(i) ∈ s_i } belongs to the indexed product filter ∏ i l_i.
Русский
Пусть имеется семейство фильтров l_i на множествах α_i и семейство подмножеств s_i such that s_i ∈ l_i для каждого i. Если все, кроме конечного числа индексов i, имеют s_i = α_i, то цилиндрическое множество {a ∈ ∏ i α_i | ∀ i, a(i) ∈ s_i} принадлежит произведению фильтров ∏ i l_i.
LaTeX
$$$\\operatorname{cofinite} \\; \\wedge \\; \\mathcal{P}(s^c) = \\operatorname{cofinite}$$$
Lean4
/-- Given a collection of filters `l i : Filter (α i)` and sets `s i ∈ l i`,
if all but finitely many of `s i` are the whole space,
then their indexed product `Set.pi Set.univ s` belongs to the filter `Filter.pi l`. -/
theorem univ_pi_mem_pi {α : ι → Type*} {s : ∀ i, Set (α i)} {l : ∀ i, Filter (α i)} (h : ∀ i, s i ∈ l i)
(hfin : ∀ᶠ i in cofinite, s i = univ) : univ.pi s ∈ pi l :=
by
filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _
if hi : s i = univ then simp [hi] else exact ha i hi
