prod_finprod_comm — Mathlib

English

For finite s, the double finprod equals the swapped order: ∑? or ∏? just as in finite products.

Русский

Для конечного множества s двойное финпроизведение равно поочередному порядку.

LaTeX

$$$(\\prod^\\!a \\in s, \\prod^\\!b \\in s, f(a,b)) = (\\prod^\\!b \\in s, \\prod^\\!a \\in s, f(a,b))$$$

Lean4

@[to_additive]
theorem prod_finprod_comm (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s, (mulSupport (f a)).Finite) :
    (∏ a ∈ s, ∏ᶠ b : β, f a b) = ∏ᶠ b : β, ∏ a ∈ s, f a b :=
  (finprod_prod_comm s (fun b a => f a b) h).symm

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