English
Let M_i be a family of monoids and consider a nonempty reduced word w from i to j. The last letter of w is defined by taking the last letter of the tail: if w is a singleton with head x, then last(w) = x; if w is w1 followed by w2, then last(w) = last(w2). In particular, the last letter of a singleton is that sole letter.
Русский
Пусть M_i — множество моноидов, образующий семейство, и пусть w — ненулевое редуцированное слово с начала i и конца j. Последняя буква слова определяется как последняя буква хвоста: для одиночного слова с головой x выполняется last(w) = x; если w имеет вид w1 и затем w2, то last(w) = last(w2). В частности, последняя буква одиночного слова равна этой букве.
LaTeX
$$$$\\text{last}(\\text{singleton}(x,a)) = x,\\quad \\text{last}(w_1 \\text{ append } w_2) = \\text{last}(w_2).$$$$
Lean4
/-- The last letter of a `NeWord` -/
@[simp]
def last : ∀ {i j} (_w : NeWord M i j), M j
| _, _, singleton x _hne1 => x
| _, _, append _w₁ _hne w₂ => w₂.last
