tail_cons

Mathlib.Data.WSeq.Basic

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

English

Let α be a type and s a WSeq α. The tail of cons(a,s) is s.

Русский

Пусть α — тип, a : α, и s — WSeq α. Хвост \text{cons}(a,s) равен s.

LaTeX

$$$$\operatorname{tail}(\operatorname{cons}(a,s)) = s.$$$$

Lean4

@[simp]
theorem tail_cons (a : α) (s) : tail (cons a s) = s := by simp [tail]

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

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

Разделы

Аффилиация

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