finprod_curry — Mathlib

English

If f: α × β → M has finite mulSupport, then the finsum over ab equals the double finsum: ∏ᶠ ab, f ab = ∏ᶠ a, b, f(a,b)

Русский

Если f: α × β → M имеет конечную мультиподдержку, то finsum над парой равен двойному finsum над координатами.

LaTeX

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

Lean4

@[to_additive]
theorem finprod_curry (f : α × β → M) (hf : (mulSupport f).Finite) : ∏ᶠ ab, f ab = ∏ᶠ (a) (b), f (a, b) :=
  by
  have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp
  have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
  simp_rw [h₂, finprod_mem_finset_product, h₁]

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