English
The product over a product set equals the product of the fiberwise products: ∏_{x ∈ s ×ˢ t} f x = ∏_{x ∈ s} ∏_{y ∈ t} f(x,y).
Русский
Произведение по множества вида произведение равно произведению по его слоям: ∏_{x ∈ s ×ˢ t} f(x) = ∏_{x ∈ s} ∏_{y ∈ t} f(x,y).
LaTeX
$$$$\\prod_{x \\in s \\timesˢ t} f(x) = \\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 = ∏ x ∈ s, ∏ y ∈ t, f (x, y) :=
prod_finset_product (s ×ˢ t) s (fun _a => t) fun _p => mem_product
