English
If s and t are disjoint subsets of β and f∘val is Multipliable on both, then the tprod over s ∪ t equals the product of the tprod over s and over t.
Русский
Если s и t — непересекающиеся подмножества β и f∘val есть Multipliable на обоих, то т-продукт по s∪t равен произведению т-продукта по s и по t.
LaTeX
$$$\\forall s t : Set β,\\ Disjoint s t → Multipliable (Function.comp f Subtype.val) → Multipliable (Function.comp f Subtype.val) → \\, \\ prod' x : ↑(s ∪ t), f x = (prod' x : s, f x) * (prod' x : t, f x)$$$
Lean4
@[to_additive]
protected theorem tprod_union_disjoint {s t : Set β} (hd : Disjoint s t) (hs : Multipliable (f ∘ (↑) : s → α))
(ht : Multipliable (f ∘ (↑) : t → α)) : ∏' x : ↑(s ∪ t), f x = (∏' x : s, f x) * ∏' x : t, f x :=
(hs.hasProd.mul_disjoint hd ht.hasProd).tprod_eq
