drop_length_sub_one — Mathlib

English

If l is nonempty, dropping the last element yields the singleton consisting of the last element: for any l ≠ [], l.drop (|l| - 1) = [last(l)].

Русский

Если список непустой, то удаление последнего элемента даёт синглтон, состоящий из последнего элемента: l.drop(|l| - 1) = [последний(l)].

LaTeX

$$$l \\neq \\emptyset \\Rightarrow l.drop (l.length - 1) = [\\mathrm{last}(l)]$$$

Lean4

theorem drop_length_sub_one {l : List α} (h : l ≠ []) : l.drop (l.length - 1) = [l.getLast h] := by
  induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]

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