leftInverse_list — Mathlib

English

The List encoding and decoding are inverse on the nose: toList(ofList γ) is the identity on lists.

Русский

Кодирование списка и декодирование обратно образуют левую обратную; toList(ofList γ)(L) = L для любого списка L.

LaTeX

$$$$\forall L:\, List(\gamma),\ \mathrm{toList}(\mathrm{ofList}(L))=L.$$$$

Lean4

theorem leftInverse_list : Function.LeftInverse (ofList γ) (toList _)
  | WType.mk Listα.nil f => by
    simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
    ext x
    cases x
  | WType.mk (Listα.cons x) f =>
    by
    simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
    rfl

Похожие утверждения