English
There exists a natural additive isomorphism that splits off the term indexed by none from a direct sum over the option-type, yielding α_none × direct_sum over the some-indices.
Русский
Существует естественный аддитивный изоморфизм, который отделяет компоненту с индексом none из прямой суммы над типом Option ι и получает α none × прямая сумма по индексам some i.
LaTeX
$$$$\\bigoplus_{i:\\mathrm{Option}\\,\\iota} \\alpha(i) \\cong_{+} \\alpha(\\mathrm{none}) \\times \\bigoplus_{i:\\iota} \\alpha(\\mathrm{some}\\,i).$$$$
Lean4
/-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`. -/
@[simps!]
noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=
{ DFinsupp.equivProdDFinsupp with map_add' := DFinsupp.equivProdDFinsupp_add }
