mem_of_mem_dropLast

Mathlib.Data.List.Infix

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

English

If a is in l.dropLast, then a is in l.

Русский

Если элемент принадлежит l.dropLast, он принадлежит l.

LaTeX

$$$\forall l : \text{List}(\alpha), \forall a : \alpha,\ a \in l.dropLast \Rightarrow a \in l.$$$

Lean4

theorem mem_of_mem_dropLast (h : a ∈ l.dropLast) : a ∈ l :=
  dropLast_subset l h

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

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

Разделы

Аффилиация

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