prod_comm — Mathlib

English

For finite index sets s ⊆ γ and t ⊆ α and a bi-variable function f: γ → α → β, the double product is commutative: ∏_{x ∈ s} ∏_{y ∈ t} f(x,y) = ∏_{y ∈ t} ∏_{x ∈ s} f(x,y).

Русский

Для конечных множеств индексов s ⊆ γ и t ⊆ α и функции f: γ → α → β выполняется двойное произведение в обычном порядке: ∏_{x ∈ s} ∏_{y ∈ t} f(x,y) = ∏_{y ∈ t} ∏_{x ∈ s} f(x,y).

LaTeX

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

Lean4

@[to_additive]
theorem prod_comm {s : Finset γ} {t : Finset α} {f : γ → α → β} : (∏ x ∈ s, ∏ y ∈ t, f x y) = ∏ y ∈ t, ∏ x ∈ s, f x y :=
  prod_comm' fun _ _ => Iff.rfl

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