English
Let s ⊆ γ and t ⊆ α, with f: γ × α → β. Then ∏_{x ∈ s} ∏_{y ∈ t} f(x,y) = ∏_{x ∈ s} ∏_{y ∈ t} f x y, i.e. the same as using a curried form.
Русский
Пусть s ⊆ γ и t ⊆ α, с f: γ × α → β. Тогда ∏_{x ∈ s} ∏_{y ∈ t} f(x,y) = ∏_{x ∈ s} ∏_{y ∈ t} f x y.
LaTeX
$$$$\\prod_{x \\in s} \\prod_{y \\in t} f(x,y) = \\prod_{x \\in s} \\prod_{y \\in t} f(x,y). $$$$
Lean4
/-- The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_product`. -/
@[to_additive /-- The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_product` -/
]
theorem prod_product' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y :=
prod_product ..
