prod_product_right — Mathlib

English

The product over a product set equals the product of the fiberwise products with the factors swapped: ∏_{x ∈ s ×ˢ t} f x = ∏_{t ∈ t} ∏_{x ∈ s} f(x,t).

Русский

Произведение по произведению множества равно произведению по волокнам со сменой порядка: ∏_{x ∈ s ×ˢ t} f x = ∏_{t ∈ t} ∏_{x ∈ s} f(x,t).

LaTeX

$$$$\\prod_{x \\in s \\timesˢ t} f(x) = \\prod_{y \\in t} \\prod_{x \\in s} f(x,y). $$$$

Lean4

@[to_additive]
theorem prod_product_right (s : Finset γ) (t : Finset α) (f : γ × α → β) :
    ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y) :=
  prod_finset_product_right (s ×ˢ t) t (fun _a => s) fun _p => mem_product.trans and_comm

Похожие утверждения