English
For finite sets s and t, the product over their union times the product over their intersection equals the product over s times the product over t: ∏_{i∈s∪t} f(i) · ∏_{i∈s∩t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Для конечных множеств s и t выполняется: произведение по их объединению умножить на произведение по их пересечению равно произведению по s умножить на произведение по t.
LaTeX
$$\left(\prod_{i \in s \cup t} f(i)\right) \left(\prod_{i \in s \cap t} f(i)\right) = \left(\prod_{i \in s} f(i)\right) \left(\prod_{i \in t} f(i)\right)$$
Lean4
/-- Given finite sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` times 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 finite sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` plus 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_inter (hs : s.Finite) (ht : t.Finite) :
((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i :=
by
lift s to Finset α using hs; lift t to Finset α using ht
classical
rw [← Finset.coe_union, ← Finset.coe_inter]
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
