dropLast_append_getLast — Mathlib

English

For any nonempty list, dropping the last element and appending the last element returns the original list; this holds by induction on length.

Русский

Для любого непустого списка удаление последнего элемента и добавление обратно последнего возвращает исходный список; доказывается по индукции по длине.

LaTeX

$$$\forall l \neq [],\ dropLast\, l ++ [\, getLast\, l] = l$$$

Lean4

theorem dropLast_append_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l ++ [getLast l h] = l
  | [], h => absurd rfl h
  | [_], _ => rfl
  | a :: b :: l, h => by
    rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]
    congr
    exact dropLast_append_getLast (cons_ne_nil b l)

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