prod_congr — Mathlib

English

If for all x ∈ supp(f) we have g1(x, f(x)) = g2(x, f(x)), then f.prod g1 = f.prod g2.

Русский

Если для всех x ∈ supp(f) выполняется g1(x, f(x)) = g2(x, f(x)), то f.prod g1 = f.prod g2.

LaTeX

$$$$ \\forall x \\in \\mathrm{supp}(f),\\ g_1(x, f(x)) = g_2(x, f(x)) \\Rightarrow f.prod g_1 = f.prod g_2 $$$$

Lean4

@[to_additive]
theorem prod_congr {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) :
    f.prod g1 = f.prod g2 :=
  Finset.prod_congr rfl h

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