tail_nil

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.tail_nil

English

Let α be a type. The tail of the empty WSeq is the empty WSeq.

Русский

Пусть α — произвольный тип. Хвост пустой WSeq равен пустому WSeq.

LaTeX

$$$$\operatorname{tail}(\mathrm{nil}) = \mathrm{nil}.$$$$

Lean4

@[simp]
theorem tail_nil : tail (nil : WSeq α) = nil := by simp [tail]

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

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

Разделы

Аффилиация

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