English
The toList representation of a NeWord starts with the pair consisting of the starting index and the word’s head. More precisely, for any w: NeWord M i j, the head of w.toList is (i, w.head) when interpreted as a list element.
Русский
Пусть w — NeWord M i j. Головной элемент списка w.toList равен пары (i, w.head), если рассмотреть элемент списка как пара. То есть начало списка отражает начальную позицию и первую букву слова.
LaTeX
$$$$w\\!\\toList\\,\\text{head}? = \\text{Some}\\langle i, w.head \\rangle.$$$$
Lean4
@[simp]
theorem toList_head? {i j} (w : NeWord M i j) : w.toList.head? = Option.some ⟨i, w.head⟩ :=
by
rw [← Option.mem_def]
induction w
· rw [Option.mem_def]
rfl
· exact List.mem_head?_append_of_mem_head? (by assumption)
