exists_of_length_succ

Mathlib.Data.List.Basic

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

← MathLib Explorer

English

If l has length n+1, then l can be written as h :: t for some h and t.

Русский

Если длина списка l равна n+1, то l можно записать как h :: t для некоторого h и t.

LaTeX

$$l.length = n + 1 → ∃ h t, l = h :: t$$

Lean4

theorem exists_of_length_succ {n} : ∀ l : List α, l.length = n + 1 → ∃ h t, l = h :: t
  | [], H => absurd H.symm <| succ_ne_zero n
  | h :: t, _ => ⟨h, t, rfl⟩

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

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

Разделы

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

Аффилиация

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