finprod_congr

Mathlib.Algebra.BigOperators.Finprod

URI: https://scilib.ai/kg/mathlib#finprod_congr

English

If f and g are pointwise equal, then finprod f equals finprod g.

Русский

Если функции f и g равны по каждой точке, то их финпроизводства равны.

LaTeX

$$$\\forall x, f x = g x \\Rightarrow \\mathrm{finprod}(f) = \\mathrm{finprod}(g)$$$

Lean4

@[to_additive]
theorem finprod_congr {f g : α → M} (h : ∀ x, f x = g x) : finprod f = finprod g :=
  congr_arg _ <| funext h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru