English
If α is a type with a decidable equality, decoding the encoding of a symmetric object on Sum (Sym (Option α) n ⊕ Sym α (n+1)) returns the original object.
Русский
Если равенство элементов в α допустимо, декодирование кодирования симметрического объекта из суммы возвращает исходный объект.
LaTeX
$$$\decode(\mathrm{encode}(s)) = s \quad\text{for } s: \mathrm{Sym}(\mathrm{Option}\,\alpha)\,n ⊕ \mathrm{Sym}\,\alpha\,(n+1)$$$
Lean4
@[simp]
theorem decode_encode [DecidableEq α] (s : Sym (Option α) n.succ) : decode (encode s) = s :=
by
by_cases h : none ∈ s
· simp [h]
· simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map, comp_apply,
Option.some_get]
convert s.attach_map_coe
