English
There is a linear isomorphism lequivProdDirectSum between the direct sum indexed by Option ι and the product of α none with the direct sum over some indices, effectively separating the none-index and the some-indices components.
Русский
Существует линейный изоморфизм lequivProdDirectSum между прямой суммой по элементам типа Option ι и произведением α none на прямую сумму по индексам some, то есть разделяет компонент none и компоненты some.
LaTeX
$$$\mathrm{lequivProdDirectSum} : (\bigoplus i, \alpha i) \simeq_\!R \alpha(\text{none}) \times (\bigoplus i, \alpha (\text{some } i)).$$$
Lean4
/-- `curryEquiv` as a linear equiv. -/
def sigmaLcurryEquiv : (⨁ i : Σ _, _, δ i.1 i.2) ≃ₗ[R] ⨁ (i) (j), δ i j :=
DFinsupp.sigmaCurryLEquiv
