English
For disjoint s and t, and finite intersections with mulSupport f, the product over s∪t equals the product over s times product over t: ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Если s и t несовпадают (Disjoint) и соответствующие пересечения с mulSupport f конечны, то ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
LaTeX
$$\operatorname{Disjoint}(s,t) \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
/-- A more general version of `finprod_mem_union` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be finite. -/
@[to_additive /-- A more general version of `finsum_mem_union` that requires `s ∩ support f` and
`t ∩ support f` rather than `s` and `t` to be finite. -/
]
theorem finprod_mem_union' (hst : Disjoint s t) (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i := by
rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty, mul_one]
