prod_product_right' — Mathlib

English

Let s ⊆ γ and t ⊆ α, f : γ × α → β. Then ∏_{x ∈ s ×ˢ t} f x = ∏_{a ∈ t} ∏_{b ∈ s} f(b,a).

Русский

Пусть s ⊆ γ и t ⊆ α, f: γ × α → β. Тогда ∏_{x ∈ s ×ˢ t} f x = ∏_{a ∈ t} ∏_{b ∈ s} f(b,a).

LaTeX

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

Lean4

/-- An uncurried version of `Finset.prod_product_right`. -/
@[to_additive /-- An uncurried version of `Finset.sum_product_right` -/
    ]
theorem prod_product_right' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
    ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y :=
  prod_product_right ..

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