getLast_concat'

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.getLast_concat'

English

The last element of concat l a is a.

Русский

Последний элемент конкатенации l и a равен a.

LaTeX

$$$\\\\mathrm{getLast}(\\\\mathrm{concat}(l,a)) = a$$$

Lean4

theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (by simp) = a := by simp

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

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

Разделы

Аффилиация

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