last_tail — Mathlib

English

If p has positive length, then the last element of p.tail equals p.last: (p.tail len_pos).last = p.last.

Русский

Если у p положительная длина, то последний элемент хвоста равен последнему элементу p: (p.tail len_pos).last = p.last.

LaTeX

$$$ (p.tail\ len_{pos}).last = p.last $$$

Lean4

@[simp]
theorem last_tail (p : RelSeries r) (len_pos : p.length ≠ 0) : (p.tail len_pos).last = p.last :=
  by
  change p _ = p _
  congr
  ext
  simp only [tail_length, Fin.val_succ, Fin.coe_cast, Fin.val_last]
  exact Nat.succ_pred_eq_of_pos (by simpa [Nat.pos_iff_ne_zero] using len_pos)

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