getLast_append_of_right_ne_nil — Mathlib

English

If l2 ≠ ∅, then getLast(l1 ++ l2) = getLast(l2).

Русский

Если правый список непуст, то последний элемент конкатенации равен последнему элементу правого списка.

LaTeX

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

Lean4

theorem getLast_append_of_right_ne_nil (l₁ l₂ : List α) (h : l₂ ≠ []) :
    getLast (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = getLast l₂ h := by induction l₁ with grind

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