finprod_mem_finset_product₃ — Mathlib

English

For a Finset of triples, the finsum equals the triple nested finsum: (∏ᶠ (a,b,c) ∈ s, f (a,b,c)) = ∏ᶠ a ∈ s, ∏ᶠ b ∈ s, ∏ᶠ c ∈ s, f(a,b,c).

Русский

Для множества тройки верно: ∏ над тройками = вложенное ∏ по каждой координате.

LaTeX

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

Lean4

@[to_additive]
theorem finprod_mem_finset_product₃ {γ : Type*} (s : Finset (α × β × γ)) (f : α × β × γ → M) :
    (∏ᶠ (abc) (_ : abc ∈ s), f abc) = ∏ᶠ (a) (b) (c) (_ : (a, b, c) ∈ s), f (a, b, c) := by
  classical
  rw [finprod_mem_finset_product']
  simp_rw [finprod_mem_finset_product']
  simp

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