toList_snoc — Mathlib

English

The toList of a snoc is the concatenation of the original toList with the new last element: (p.snoc newLast rel).toList = p.toList ++ [newLast].

Русский

ToList от snoc равен конкатенации ToList исходной последовательности и нового последнего элемента: (p.snoc newLast rel).toList = p.toList ++ [newLast].

LaTeX

$$$ (p.snoc newLast rel).toList = p.toList \cup \{ newLast \} $$$

Lean4

@[simp]
theorem toList_snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) :
    (p.snoc newLast rel).toList = p.toList ++ [newLast] := by simp [snoc]

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