dropLast_append_getLast? — Mathlib

English

Another variant of appending a last element to dropLast to recover the original list.

Русский

Ещё один вариант восстановления исходного списка через удаление и добавление последнего элемента.

LaTeX

$$$\forall l\ a,\ a \in l.getLast? \Rightarrow\ dropLast l ++ [a] = l$$$

Lean4

theorem dropLast_append_getLast? : ∀ {l : List α}, ∀ a ∈ l.getLast?, dropLast l ++ [a] = l
  | [], a, ha => (Option.not_mem_none a ha).elim
  | [a], _, rfl => rfl
  | a :: b :: l, c, hc => by
    rw [getLast?_cons_cons] at hc
    rw [dropLast_cons₂, cons_append, dropLast_append_getLast? _ hc]

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