prod_congr — Mathlib

English

If s1 = s2 and f = g on s2, then the products over s1 and s2 with respective functions are equal.

Русский

Если множества s1 и s2 равны, и функции совпадают на s2, то соответствующие произведения равны.

LaTeX

$$$s_1 = s_2 \\Rightarrow (\\forall x \\in s_2, f(x)=g(x)) \\Rightarrow \\prod_{x \\in s_1} f(x) = \\prod_{x \\in s_2} g(x)$$$

Lean4

@[to_additive (attr := congr)]
theorem prod_congr (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g := by rw [h]; exact fold_congr

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