English
If s ⊆ t and t is finite, then (∏ᶠ i ∈ s, f i) · (∏ᶠ i ∈ t \\ s, f i) = ∏ᶠ i ∈ t, f i.
Русский
Если s ⊆ t и t конечно, то произведение по s и произведение по t\\s перемножаются в произведение по t.
LaTeX
$$$\\Big(\\prod^\\!i \\in s, f(i)\\Big) \\cdot \\Big(\\prod^\\!i \\in t \\setminus s, f(i)\\Big) = \\prod^\\!i \\in t, f(i)$$$
Lean4
@[to_additive]
theorem finprod_mem_inter_mul_diff (t : Set α) (h : s.Finite) :
((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i :=
finprod_mem_inter_mul_diff' _ <| h.inter_of_left _