ofStream_cons

Mathlib.Data.Seq.Basic

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

← MathLib Explorer

English

The length of s.take n is at most n.

Русский

Длина выборки take составляет не более n.

LaTeX

$$$(s.take n).length \le n$$$

Lean4

@[simp]
theorem ofStream_cons (a : α) (s) : ofStream (a :: s) = cons a (ofStream s) := by apply Subtype.eq;
  simp only [ofStream, cons]; rw [Stream'.map_cons]

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

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

Разделы

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

Аффилиация

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