last_eraseLast — Mathlib

English

In a nontrivial RelSeries p, eraseLast preserves a relation between the new last element and the previous last: p.eraseLast.last ~[r] p.last.

Русский

В ненулевой RelSeries p eraseLast сохраняет отношение между новым последним и прежним последним: p.eraseLast.last ~[r] p.last.

LaTeX

$$$ p.eraseLast.last \sim{_r} p.last $$$

Lean4

@[simp]
theorem last_eraseLast (p : RelSeries r) : p.eraseLast.last = p ⟨p.length.pred, Nat.lt_succ_iff.2 (Nat.pred_le _)⟩ :=
  rfl

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