cons_self_tail — Mathlib

English

If p has positive length, then (p.tail hp).cons p.head (p.3 ⟨0, ...⟩) = p, i.e., pulling the tail and then re-adding the head recovers p.

Русский

Если p имеет положительную длину, то (p.tail hp).cons p.head (... ) = p, то есть вынеся хвост и заново добавляя голову, получаем p.

LaTeX

$$$ (p.tail hp).\text{cons } p.head (p.3 ⟨0, \dots⟩) = p $$$

Lean4

theorem cons_self_tail {p : RelSeries r} (hp : p.length ≠ 0) :
    (p.tail hp).cons p.head (p.3 ⟨0, Nat.zero_lt_of_ne_zero hp⟩) = p :=
  by
  apply toList_injective
  simp [← head_toList]

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