getLast_append_singleton

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.getLast_append_singleton

English

The last element of l concatenated with a singleton [a] is a.

Русский

Последний элемент списка l, дополненного единичным списком [a], равен a.

LaTeX

$$$\\\\mathrm{getLast}(l \\\\;\\\\,+\\\\; [a]) = a$$$

Lean4

theorem getLast_append_singleton {a : α} (l : List α) :
    getLast (l ++ [a]) (append_ne_nil_of_right_ne_nil l (cons_ne_nil a _)) = a := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru