English
Inverse of the decoding bijection for the sum of Sym structures: it maps a sum of Sym(Option α) and Sym α into Sym (Option α) after consuming the option structure.
Русский
Обратная к биекции декодирования для суммы структур Sym: отображает сумму Sym(Option α) и Sym α в Sym(Option α).
LaTeX
$$$\\text{decode} : \\mathrm{Sym}(\\mathrm{Option}\\\\alpha)\\ n \\oplus \\mathrm{Sym}\\alpha\\ n.\\mathrm{succ} \\to \\mathrm{Sym}(\\mathrm{Option}\\alpha)\\ n.\\mathrm{succ}$ является обратной к каноническому биекция паміж ними.$$
Lean4
/-- Inverse of `Sym_option_succ_equiv.decode`. -/
def decode : Sym (Option α) n ⊕ Sym α n.succ → Sym (Option α) n.succ
| Sum.inl s => none ::ₛ s
| Sum.inr s => s.map Embedding.some
