English
Let ι be a finite index set and for each i ∈ ι let S_i ⊆ α. Then the set of all products ∏_{i ∈ ι} x_i with x_i ∈ S_i for every i equals the Cartesian product ∏_{i ∈ ι} S_i.
Русский
Пусть ι — конечный индексный множественный набор, и для каждого i ∈ ι задано S_i ⊆ α. Тогда множество всех произведений ∏_{i ∈ ι} x_i, где x_i ∈ S_i, равно декартовому произведению ∏_{i ∈ ι} S_i.
LaTeX
$$$$ \\left\\{ \\prod_{i \\in \\mathcal{I}} f(i) \\;:\\; f:\\mathcal{I} \\to \\alpha,\ \forall i \\in \\mathcal{I},\\ f(i) \\in S_i \\right\\} = \\prod_{i \\in \\mathcal{I}} S_i $$$$
Lean4
/-- A special case of `Set.image_finset_prod_pi` for `Finset.univ`. -/
@[to_additive /-- A special case of `Set.image_finset_sum_pi` for `Finset.univ`. -/
]
theorem image_fintype_prod_pi [Fintype ι] (S : ι → Set α) : (fun f : ι → α => ∏ i, f i) '' univ.pi S = ∏ i, S i := by
simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S
