cons_ne_nil

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.cons_ne_nil

English

For any x and s, the constructed sequence cons x s is not equal to nil.

Русский

Для любых x и s последовательность, построенная как cons x s, не равна nil.

LaTeX

$$$\\forall x:\\alpha\\,\\forall s:\\mathrm{Seq}\\alpha,\\; (\\mathrm{cons}\\ x\\ s) \\neq \\mathrm{nil}$$$

Lean4

@[simp]
theorem cons_ne_nil {x : α} {s : Seq α} : (cons x s) ≠ .nil :=
  by
  intro h
  simpa using congrArg (·.get? 0) h

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

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

Разделы

Аффилиация

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