ofList_cons — Mathlib

English

ofList respects cons: ofList (a :: l) = cons a (ofList l).

Русский

ofList сохраняет операции добавления в начало: ofList (a :: l) = cons a (ofList l).

LaTeX

$$$$\mathrm{ofList}(\mathrm{List}.cons\,a\,l) = \mathrm{Stream'.WSeq}.cons\,a\,(\mathrm{ofList}\,l).$$$$

Lean4

@[simp]
theorem ofList_cons (a : α) (l) : ofList (a :: l) = cons a (ofList l) :=
  show Seq.map some (Seq.ofList (a :: l)) = Seq.cons (some a) (Seq.map some (Seq.ofList l)) by simp

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