cons_head?_tail

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.cons_head?_tail

← MathLib Explorer

English

If a ∈ head? l, then a :: tail l = l.

Русский

Если a принадлежит head? списка l, то l = a :: tail l.

LaTeX

$$$\\\\forall {l} {a}, a \\\\in head? l \\\\Rightarrow \\\\; a \\\\;:: tail l = l$$$

Lean4

theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l
  | [], a, h => by contradiction
  | b :: l, a, h => by
    have : b = a := by simpa using h
    simp [this]

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

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

Разделы

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

Аффилиация

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