toList_getLast? — Mathlib

English

The last element of w.toList is Some(⟨j, w.last⟩). In particular, the final element of the list corresponds to the final index and the final letter of the word.

Русский

Последний элемент w.toList равен Some(⟨j, w.last⟩). Следовательно, завершающий элемент списка задаёт конечный индекс и последнюю букву слова.

LaTeX

$$$$w.toList.getLast? = \\text{Some}\\langle j, w.last \\rangle.$$$$

Lean4

@[simp]
theorem toList_getLast? {i j} (w : NeWord M i j) : w.toList.getLast? = Option.some ⟨j, w.last⟩ :=
  by
  rw [← Option.mem_def]
  induction w
  · rw [Option.mem_def]
    rfl
  · exact List.mem_getLast?_append_of_mem_getLast? (by assumption)

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