English
Two finite sets s,t with the property that Disjoint(s ∩ mulSupport f, t ∩ mulSupport f) hold yield ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Два конечных множества s, t с условием Disjoint(s∩mulSupport f, t∩mulSupport f) дают равенство произведений над s∪t и над s,t.
LaTeX
$$\operatorname{Disjoint}(s \cap \operatorname{mulSupport} f, t \cap \operatorname{mulSupport} f) \Rightarrow \prod_{i \in s \cup t} f(i) = \left(\prod_{i \in s} f(i)\right) \left(\prod_{i \in t} f(i)\right)$$
Lean4
/-- Given two finite disjoint sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` equals the
product of `f i` over `i ∈ s` times the product of `f i` over `i ∈ t`. -/
@[to_additive /-- Given two finite disjoint sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` equals
the sum of `f i` over `i ∈ s` plus the sum of `f i` over `i ∈ t`. -/
]
theorem finprod_mem_union (hst : Disjoint s t) (hs : s.Finite) (ht : t.Finite) :
∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i :=
finprod_mem_union' hst (hs.inter_of_left _) (ht.inter_of_left _)
