ofList_cons — Mathlib

English

Prepending an element to a list corresponds to prepending the same element to the corresponding sequence.

Русский

Добавление элемента в начало списка соответствует добавлению того же элемента в начало соответствующей последовательности.

LaTeX

$$$ \forall a:\alpha\, \forall l:\mathrm{List}(\alpha),\ \mathrm{ofList}(\mathrm{List.cons}(a,l)) = \mathrm{cons}(a,\mathrm{ofList}(l)).$$$

Lean4

@[simp]
theorem ofList_cons (a : α) (l : List α) : ofList (a :: l) = cons a (ofList l) := by ext1 (_ | n) <;> simp

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