head!_mem_self

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.head!_mem_self

← MathLib Explorer

English

head! _mem_self: head! l ∈ l for any nonempty l.

Русский

head! l принадлежит списку l для непустого l.

LaTeX

$$$\\\\mathrm{head!}(l) \\\\in l$$$

Lean4

theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! ∈ l :=
  by
  have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self
  rwa [cons_head!_tail h] at h'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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