English
There is a canonical equivalence between finsupp over a dependent sum and a dependent product of finsupps, provided the index type is finite.
Русский
Существует каноническое эквивалентность между финспп над зависимой суммой и зависимым произведением финспп при конечном множестве индексов.
LaTeX
$$$\\sigmaFinsuppEquivPiFinsupp : ((\\\\Sigma j, ιs j) \\\\to_0 α) \\\\simeq ∀ j, ιs j \\\\to_0 α$$$
Lean4
/-- On a `Fintype η`, `Finsupp.split` is an equivalence between `(Σ (j : η), ιs j) →₀ α`
and `Π j, (ιs j →₀ α)`.
This is the `Finsupp` version of `Equiv.Pi_curry`. -/
noncomputable def sigmaFinsuppEquivPiFinsupp : ((Σ j, ιs j) →₀ α) ≃ ∀ j, ιs j →₀ α
where
toFun := split
invFun
f :=
onFinset (Finset.univ.sigma fun j => (f j).support) (fun ji => f ji.1 ji.2) fun _ hg =>
Finset.mem_sigma.mpr ⟨Finset.mem_univ _, mem_support_iff.mpr hg⟩
left_inv
f := by
ext
simp [split]
right_inv
f := by
ext
simp [split]
