English
Let f: β → α be a function into a commutative topological group α, with α complete under multiplication. For any finite subset s ⊆ β, the infinite product over β is multipliable iff the product over β outside s is multipliable. In symbols, the multipliability of f on β is equivalent to the multipliability of f restricted to β \ s.
Русский
Пусть f: β → α — функция в коммутативной топологической группе α. Для любого конечного подмножества s ⊆ β последовательность бесконечного произведения f(b) по b ∈ β сходится тогда и только тогда, когда произведение по всем b, не входящим в s, сходится; то есть умножаемость сохраняется при удалении конечного множества индексов.
LaTeX
$$$ \\forall s \\subseteq_f \\beta: \\ Multipliable \\bigl(f\\bigr) \\iff \\ Multipliable \\bigl(f\\restriction (\\beta \\setminus s)\\bigr).$$$
Lean4
@[to_additive]
protected theorem multipliable_compl_iff (s : Finset β) :
(Multipliable fun x : { x // x ∉ s } ↦ f x) ↔ Multipliable f :=
(s.multipliable f).multipliable_compl_iff
