English
If f and g are Multipliable with respect to a summation filter L, then the tprod of their pointwise products equals the product of their tprod: ∏'[L] b, f b * g b = (∏'[L] b, f b) · (∏'[L] b, g b).
Русский
Пусть f и g над β упорядочены так, что их бесконечные произведения сходятся относительно фильтра суммирования L. Тогда т-продукт точечной умножения равен произведению их т-продуктов: ∏' f b g b = (∏ f b)(∏ g b).
LaTeX
$$$\\forall {f,g},\\ [L \\text{ NeBot}]\\ (hf : Multipliable f\\, L) (hg : Multipliable g\\, L) : \\\\ \\prod'[L] b, (f b * g b) = (\\prod'[L] b, f b) \\, * \\, (\\prod'[L] b, g b)$$$
Lean4
@[to_additive]
protected theorem tprod_mul [L.NeBot] (hf : Multipliable f L) (hg : Multipliable g L) :
∏'[L] b, (f b * g b) = (∏'[L] b, f b) * ∏'[L] b, g b :=
(hf.hasProd.mul hg.hasProd).tprod_eq
