English
Let f be a function, and s ⊆ β. If the restrictions of f to s and to the complement of s are Multipliable with respect to L, then the total tprod over β equals the product of the tprod over s and over the complement.
Русский
Пусть f: β → α. Если ограничения f на множество s и на дополнение к s являются Multipliable относительно фильтра L, то общий т-продукт по β равен произведению т-продуктов по s и по комплементу.
LaTeX
$$$\\forall s: Set\\,β,\\ (hs: Multipliable (f \\circ (↑) : s \\to α)) (hsc: Multipliable (f \\circ (↑) : ↑s^c \\to α)) :\\ (∏' x : s, f x) * ∏' x : ↑s^c, f x = ∏' x, f x$$$
Lean4
@[to_additive]
protected theorem tprod_mul_tprod_compl {s : Set β} (hs : Multipliable (f ∘ (↑) : s → α))
(hsc : Multipliable (f ∘ (↑) : ↑sᶜ → α)) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x :=
(hs.hasProd.mul_compl hsc.hasProd).tprod_eq.symm
