English
Conversely, encoding the result of decoding a sum object yields the original sum object.
Русский
Напротив, кодирование результата декодирования симметрического объекта из суммы возвращает исходный объект.
LaTeX
$$$\encode(\decode(s)) = s$$$
Lean4
@[simp]
theorem encode_decode [DecidableEq α] (s : Sym (Option α) n ⊕ Sym α n.succ) : encode (decode s) = s :=
by
obtain s | s := s
· simp
· unfold SymOptionSuccEquiv.encode
split_ifs with h
· obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
exact Option.some_ne_none _ ha
· refine congr_arg Sum.inr ?_
refine map_injective (Option.some_injective _) _ ?_
refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_) <;> simp
