ofList_toList — Mathlib

English

Let s be a terminating sequence. Then the finite list produced by toList(s) can be converted back to the original sequence by ofList, i.e., ofList (toList s h) = s for any terminating proof h.

Русский

Пусть s — завершаемая последовательность. Тогда список, получаемый через toList, может быть преобразован обратно в последовательность с помощью ofList, то есть ofList (toList s h) = s для любого доказательства завершения h.

LaTeX

$$$\forall {\alpha} (s : Seq \alpha) (h : s.Terminates),\; ofList (toList s h) = s$$$

Lean4

@[simp]
theorem ofList_toList (s : Seq α) (h : s.Terminates) : ofList (toList s h) = s := by ext n; simp [ofList]

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