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
/-- If `s : Set α` and `t : Set β` are finite sets, then taking the product over `s` commutes with
taking the product over `t`. -/
@[to_additive /-- If `s : Set α` and `t : Set β` are finite sets, then summing over `s` commutes with
summing over `t`. -/
]
theorem finprod_mem_comm {s : Set α} {t : Set β} (f : α → β → M) (hs : s.Finite) (ht : t.Finite) :
(∏ᶠ i ∈ s, ∏ᶠ j ∈ t, f i j) = ∏ᶠ j ∈ t, ∏ᶠ i ∈ s, f i j :=
by
lift s to Finset α using hs; lift t to Finset β using ht
simp only [finprod_mem_coe_finset]
exact Finset.prod_comm
