English
The indexed product of pure filters pi (pure f_i) is characterized by finite support cylinders.
Русский
Произведение чистых фильтров имеет характеристику через цилиндры с конечной поддержкой.
LaTeX
$$$s \in \pi (\lambda i. \text{pure}(f_i)) \iff \exists I, I.Finite \land \forall g, (\forall i \in I, g_i = f_i) \rightarrow g \in s$$$
Lean4
/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.
If the index type is finite, then the indexed product of principal filters
is a principal filter, see `pi_principal`. -/
theorem mem_pi_principal {t : Set ((i : ι) → α i)} : t ∈ pi (fun i ↦ 𝓟 (s i)) ↔ ∃ I : Set ι, I.Finite ∧ I.pi s ⊆ t :=
(hasBasis_pi (fun i ↦ hasBasis_principal _)).mem_iff.trans <| by simp
