cons_getLast_dropLast — Mathlib

English

If L is nonempty, the list formed by taking the last element of L and placing it at the front is a rotation of L.

Русский

Пусть L непуст; список, состоящий из последнего элемента L перед всеми остальными, является поворотом L.

LaTeX

$$$L.getLast(hL) :: L.dropLast ~r L$$$

Lean4

theorem cons_getLast_dropLast (L : List α) (hL : L ≠ []) : L.getLast hL :: L.dropLast ~r L := by
  induction L using List.reverseRecOn with
  | nil => simp at hL
  | append_singleton a L _ =>
    simp only [getLast_append, dropLast_concat]
    apply IsRotated.symm
    apply isRotated_concat

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