cons_not_terminatedAt_zero

Mathlib.Data.Seq.Defs

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

English

For any x and s, the sequence cons x s is not terminated at position 0.

Русский

Для любых x и s последовательность cons x s не завершается на позиции 0.

LaTeX

$$$\\neg (\\mathrm{cons}(x,s)).\\TerminatedAt(0)$$$

Lean4

@[simp]
theorem cons_not_terminatedAt_zero {x : α} {s : Seq α} : ¬(cons x s).TerminatedAt 0 := by simp [TerminatedAt]

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

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

Разделы

Аффилиация

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