English
If s ⊆ t and (t ∩ mulSupport f).Finite, then (∏ᶠ i ∈ s, f i) · (∏ᶠ i ∈ t \\ s, f i) = ∏ᶠ i ∈ t, f i.
Русский
Если s ⊆ t и (t ∩ supp f) конечно, то произведение по 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
/-- Given a finite set `t` and a subset `s` of `t`, the product of `f i` over `i ∈ s`
times the product of `f i` over `t \ s` equals the product of `f i` over `i ∈ t`. -/
@[to_additive /-- Given a finite set `t` and a subset `s` of `t`, the sum of `f i` over `i ∈ s` plus
the sum of `f i` over `t \ s` equals the sum of `f i` over `i ∈ t`. -/
]
theorem finprod_mem_mul_diff (hst : s ⊆ t) (ht : t.Finite) : ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i :=
finprod_mem_mul_diff' hst (ht.inter_of_left _)
