English
There is a bijection between finsupps on Option α with values in M and pairs (m, f) with m ∈ M and f ∈ α →₀ M; the map toFun sends P to (P none, P.some) and the inverse sends (m,f) to (f.embDomain .some).update none P.1.
Русский
Существует биекция между финспфами на Option α с значениями в M и парами (m, f) из M и α →₀ M; отображение в сторону пары задается через (P none, P.some), обратное отображение строится через (f.embDomain .some).update none m.
LaTeX
$$$ \text{optionEquiv} : (\mathrm{Option}\;\alpha \to_0 M) \simeq M \times (\alpha \to_0 M) $$$
Lean4
/-- `Finsupp`s from `Option` are equivalent to
pairs of an element and a `Finsupp` on the original type. -/
@[simps]
noncomputable def optionEquiv [Zero M] : (Option α →₀ M) ≃ M × (α →₀ M)
where
toFun P := (P none, P.some)
invFun P := (P.2.embDomain .some).update none P.1
left_inv P := by ext (_ | a) <;> simp [Finsupp.update]
right_inv P := by ext <;> simp [Finsupp.update]
