English
Characterizes membership in the Pi-filter of principal(s) by the finite cylinder condition.
Русский
Характеризует членство в Pi-фильтре главных цилиндров через конечные цилиндры.
LaTeX
$$$t \in \pi(\mathrm{fun i => \mathfrak{P}(s_i)}) \iff \exists I, I.Finite \wedge I.pi(s) ⊆ t$$$
Lean4
/-- The indexed product of finitely many principal filters
is the principal filter corresponding to the cylinder `Set.univ.pi s`.
If the index type is infinite, then `mem_pi_principal` and `hasBasis_pi_principal` may be useful. -/
@[simp]
theorem pi_principal [Finite ι] (s : (i : ι) → Set (α i)) : pi (fun i ↦ 𝓟 (s i)) = 𝓟 (univ.pi s) := by
simp [Filter.pi, Set.pi_def]
