toList_ofList — Mathlib

English

For any finite list l, if we form a stream from it and then convert back to a list, we obtain l again.

Русский

Для любого конечного списка l, если построить поток из него, а затем снова преобразовать в список, получится тот же l.

LaTeX

$$$\forall l : List \alpha, toList (ofList l) (terminates_ofList l) = l$$$

Lean4

@[simp]
theorem toList_ofList (l : List α) : toList (ofList l) (terminates_ofList l) = l :=
  ofList_injective (by simp)

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