head_tail — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem head_tail (p : RelSeries r) (len_pos : p.length ≠ 0) : (p.tail len_pos).head = p 1 :=
  by
  change p (Fin.succ _) = p 1
  congr
  ext
  change (1 : ℕ) = (1 : ℕ) % _
  rw [Nat.mod_eq_of_lt]
  simpa only [lt_add_iff_pos_left, Nat.pos_iff_ne_zero]

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