toList_ofList

Mathlib.Data.WSeq.Basic

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

← MathLib Explorer

English

For every list l, l belongs to the output toList(ofList l).

Русский

Для любого списка l, l принадлежит результату toList(ofList l).

LaTeX

$$$$\forall l:\\mathrm{List}\,\alpha,\ l \in toList(\\mathrm{ofList}\,l).$$$$

Lean4

theorem toList_ofList (l : List α) : l ∈ toList (ofList l) := by
  induction l with
  | nil => simp
  | cons a l IH => simpa [ret_mem] using think_mem (Computation.mem_map _ IH)

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

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

Разделы

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

Аффилиация

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