tprod_congr — Mathlib

English

Let α be a topological commutative monoid and L a summation filter on β. If two functions f, g: β → α are equal at every point, then their tprod over L are equal: ∏'_{L} b, f(b) = ∏'_{L} b, g(b).

Русский

Пусть α — коммутативная моноидальная топология, L — фильтр суммирования на β. Если функции f,g: β → α совпадают при каждой точке, то их бесконечный т-произведение по L совпадает: ∏'_L b, f(b) = ∏'_L b, g(b).

LaTeX

$$$\\\\prod'_{L} b \\, f(b) = \\\\prod'_{L} b \\, g(b)$$$

Lean4

@[to_additive]
theorem tprod_congr {f g : β → α} (hfg : ∀ b, f b = g b) : ∏'[L] b, f b = ∏'[L] b, g b :=
  congr_arg (tprod · L) (funext hfg)

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