English
For s ⊆ t and (t ∩ mulSupport f).Finite, the product over s of f times the product over t\\s equals the product over t.
Русский
Для s ⊆ t и конечности пересечения t с поддержкой 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
/-- A more general version of `finprod_mem_mul_diff` that requires `t ∩ mulSupport f` rather than
`t` to be finite. -/
@[to_additive /-- A more general version of `finsum_mem_add_diff` that requires `t ∩ support f` rather
than `t` to be finite. -/
]
theorem finprod_mem_mul_diff' (hst : s ⊆ t) (ht : (t ∩ mulSupport f).Finite) :
((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i := by
rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]
