head_snoc — Mathlib

English

Prepending a new last element to a RelSeries does not change its head: (p.snoc newLast rel).head = p.head.

Русский

Добавление нового последнего элемента слева не меняет головы последовательности: (p.snoc newLast rel).head = p.head.

LaTeX

$$$ (p.\text{snoc } newLast\ rel).\text{head} = p.\text{head} $$$

Lean4

@[simp]
theorem head_snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) : (p.snoc newLast rel).head = p.head := by
  delta snoc; rw [head_append]

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