finprod_mem_finset_product — Mathlib

English

For a finite set s of pairs, the finsum over s equals the nested finsum over coordinates: (∏ᶠ (ab) ∈ s, f ab) = ∏ᶠ (a,b) ∈ s, f (a,b).

Русский

Для конечного множества пар сумма по парам равна вложенной сумме по координатам: (∏ᶠ (ab) ∈ s, f(ab)) = ∏ᶠ (a,b) ∈ s, f(a,b).

LaTeX

$$$ (\\\\prod^\\\\mathrm{f} (ab) (ab \\in s), f(ab)) = \\\\prod^\\\\mathrm{f} (a) (b) (b \\in s), f(a,b) $$$

Lean4

/-- See also `finprod_mem_finset_product'`. -/
@[to_additive /-- See also `finsum_mem_finset_product'`. -/
    ]
theorem finprod_mem_finset_product (s : Finset (α × β)) (f : α × β → M) :
    (∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : (a, b) ∈ s), f (a, b) := by
  classical
  rw [finprod_mem_finset_product']
  simp

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