append_last — Mathlib

English

The last of an appended NeWord is the last of the second part: last(append w1 hne w2) = last(w2).

Русский

Последняя буква объединённого слова — последняя буква второго слагаемого: last(append w1 hne w2) = last(w2).

LaTeX

$$$$\\text{last}(\\text{append}(w_1,\\, hne, w_2)) = w_2.last.$$$$

Lean4

@[simp]
theorem append_last {i j k l} {w₁ : NeWord M i j} {hne : j ≠ k} {w₂ : NeWord M k l} :
    (append w₁ hne w₂).last = w₂.last :=
  rfl

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