toList_cons — Mathlib

English

The toList of a cons-constructed series equals the list with the new head prepended to the original toList.

Русский

toList серии, построенной конc-операцией, равен списку, полученному добавлением новой головы слева к исходному toList.

LaTeX

$$$ (p.cons x hx).toList = x :: p.toList $$$

Lean4

@[simp]
theorem toList_cons (p : RelSeries r) (x : α) (hx : x ~[r] p.head) : (p.cons x hx).toList = x :: p.toList :=
  by
  rw [cons, toList_append]
  simp

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