English
For finite index Finsets of pairs, the finsum over pairs equals a nested finsum over coordinates: (∏ᶠ (ab) ∈ s, f ab) = ∏ᶠ a (b) (b ∈ (s.filter (fst ab = a)).image snd), f (a,b).
Русский
Для конечного множества пар сумма по парам равна вложенной сумме по координатам: (∏ᶠ (ab) ∈ s, f(ab)) = ∏ᶠ a (b) (b ∈ (s.filter (fst ab = a)).image snd), f(a,b).
LaTeX
$$$ (\\\\prod^\\\\mathrm{f} (ab) (ab \\in s), f(ab)) = \\\\prod^\\\\mathrm{f} a (b) (b \\in (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd), f(a,b) $$$
Lean4
/-- Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
we can simplify the right-hand side of this lemma. However the form stated here is more useful for
iterating this lemma, e.g., if we have `f : α × β × γ → M`. -/
@[to_additive /-- Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
we can simplify the right-hand side of this lemma. However the form stated here is more
useful for iterating this lemma, e.g., if we have `f : α × β × γ → M`. -/
]
theorem finprod_mem_finset_product' [DecidableEq α] [DecidableEq β] (s : Finset (α × β)) (f : α × β → M) :
(∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : b ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd), f (a, b) :=
by
have (a : _) :
∏ i ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i) = (s.filter (Prod.fst · = a)).prod f := by
refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop
rw [finprod_mem_finset_eq_prod]
simp_rw [finprod_mem_finset_eq_prod, this]
rw [finprod_eq_prod_of_mulSupport_subset _ (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst), ←
Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]
-- `finish` could close the goal here
simp only [Finset.mem_image]
exact fun x hx => ⟨x, hx, rfl⟩
