English
A more general version: for f, and finite s,t restricted to mulSupport f, the same product equality holds: ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Обобщение: для функции f и конечных s,t в отношении mulSupport f выполняется равенство произведений над объединением и пересечением аналогично выше.
LaTeX
$$\operatorname{Finite}((s\cup 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
/-- A more general version of `finprod_mem_union_inter` 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_inter` that requires `s ∩ support f` and
`t ∩ support f` rather than `s` and `t` to be finite. -/
]
theorem finprod_mem_union_inter' (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ 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_inter hs ht, ←
union_inter_distrib_right, finprod_mem_inter_mulSupport, ← finprod_mem_inter_mulSupport f (s ∩ t)]
rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
