append_singleton_left — Mathlib

English

Prepending a singleton chain to p is the same as cons-ing the head element: (singleton x).append p hx = p.cons x hx.

Русский

Добавление слева одиночной цепи к p эквивалентно операцию cons над головой: (singleton x).append p hx = p.cons x hx.

LaTeX

$$$ (singleton r x).append p hx = p.cons x hx $$$

Lean4

@[simp]
theorem append_singleton_left (p : RelSeries r) (x : α) (hx : x ~[r] p.head) :
    (singleton r x).append p hx = p.cons x hx :=
  rfl

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