English
There is a natural equivalence between the dfinsupp over Σ i α_i and the dfinsupp of dfinsupps, given by sigmaCurry and sigmaUncurry as inverse.
Русский
Существует естественное эквивалентное соответствие между dfinsupp над Σ i α_i и dfinsupp над dfinsuppами; карри-сигма и развёртывание обратны друг другу.
LaTeX
$$$\sigma\text{-CurryEquiv} : (\Pi_0 i : \Sigma _, _, δ i.1 i.2) \simeq (\Pi_0 i (j), δ i j)$$$
Lean4
/-- The natural bijection between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.
This is the dfinsupp version of `Equiv.piCurry`. -/
def sigmaCurryEquiv [∀ i j, Zero (δ i j)] [DecidableEq ι] : (Π₀ i : Σ _, _, δ i.1 i.2) ≃ Π₀ (i) (j), δ i j
where
toFun := sigmaCurry
invFun := sigmaUncurry
left_inv
f := by
ext ⟨i, j⟩
rw [sigmaUncurry_apply, sigmaCurry_apply]
right_inv
f := by
ext i j
rw [sigmaCurry_apply, sigmaUncurry_apply]
