English
The prime version mem_pi' states that membership in pi f is equivalent to the existence of a finite index set I and a t such that for all i, t i ∈ f i and I.pi t ⊆ s.
Русский
Версия mem_pi' говорит: членство в pi f эквивалентно существованию конечного множества индексов I и t с t_i ∈ f_i и I.pi t ⊆ s.
LaTeX
$$$s \in \pi f \iff \exists I : Finset ι, \exists t : \forall i, Set(α_i), (\forall i, t_i \in f_i) ∧ (I.toSet).pi t ⊆ s$$$
Lean4
theorem mem_pi' {s : Set (∀ i, α i)} :
s ∈ pi f ↔ ∃ I : Finset ι, ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ Set.pi (↑I) t ⊆ s :=
mem_pi.trans exists_finite_iff_finset
