English
snoc extends a RelSeries by appending a new last element, given a relation between the previous last and the new last.
Русский
snoc добавляет новый последний элемент к RelSeries, если существует связь между предыдущим последним и новым.
LaTeX
$$def snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) : RelSeries r := p.append (singleton r newLast) rel$$
Lean4
/-- Given a series `a₀ -r→ a₁ -r→ ... -r→ aₙ` and an `a` such that `aₙ -r→ a` holds, there is
a series of length `n+1`: `a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a`.
-/
@[simps! length]
def snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) : RelSeries r :=
p.append (singleton r newLast) rel
