English
A refined version: for f and finite s,t with (s ∩ mulSupport f) finite and (t ∩ mulSupport f) finite, the same union-intersection product rule holds: ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Уточнённая версия: для f, конечных s,t и условий (s∩mulSupport f) конечно и (t∩mulSupport f) конечно выполняется правило произведений над объединением и пересечением.
LaTeX
$$\left( (s \cap \operatorname{mulSupport} f) \right).Finite \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 disjoint -/
@[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 disjoint -/
]
theorem finprod_mem_union'' (hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)) (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_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ← finprod_mem_union hst hs ht, ←
union_inter_distrib_right, finprod_mem_inter_mulSupport]
