getLast?_append_of_ne_nil — Mathlib

English

For l1, if l2 ≠ ∅, getLast? (l1 ++ l2) = getLast? l2.

Русский

Для списка l1 и непустого l2, последний элемент конкатенации равен последнему элементу l2.

LaTeX

$$$\\\\mathrm{getLast}? (l_1 \\\\; ++ \\\\; l_2) = \\\\mathrm{getLast}? l_2 \\\\;\\\\text{ when } l_2 \\\\neq \\\\emptyset$$$

Lean4

theorem getLast?_append_of_ne_nil (l₁ : List α) : ∀ {l₂ : List α} (_ : l₂ ≠ []), getLast? (l₁ ++ l₂) = getLast? l₂
  | [], hl₂ => by contradiction
  | b :: l₂, _ => getLast?_append_cons l₁ b l₂

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