getLast?_toList — Mathlib

English

The last element of the toList representation of a terminating stream coincides with the last element of the stream itself.

Русский

Последний элемент списка, полученного через toList, совпадает с последним элементом последовательности.

LaTeX

$$$(toList s h).getLast? = s.get? (s.length h - 1)$$$

Lean4

theorem getLast?_toList (s : Seq α) (h : s.Terminates) : (toList s h).getLast? = s.get? (s.length h - 1) := by
  rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]

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