eraseLast_last_rel_last — Mathlib

English

For p with length nonzero, eraseLast converts the list to the original list with the last element removed: eraseLast.toList = toList.dropLast.

Русский

Для p с ненулевой длиной eraseLast переводит список в исходный без последнего элемента: eraseLast.toList = toList.dropLast.

LaTeX

$$$ p.eraseLast.toList = p.toList.dropLast $$$

Lean4

/-- In a non-trivial series `p`, the last element of `p.eraseLast` is related to `p.last` -/
theorem eraseLast_last_rel_last (p : RelSeries r) (h : p.length ≠ 0) : p.eraseLast.last ~[r] p.last :=
  by
  simp only [last, Fin.last, eraseLast_length, eraseLast_toFun]
  convert p.step ⟨p.length - 1, by cutsat⟩
  simp only [Fin.succ_mk]; cutsat

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