tail_cons

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.tail_cons

English

Tail of a cons is equal to the original series: (p.cons x hx).tail = p.

Русский

Хвост от конструирования cons равен исходной последовательности: (p.cons x hx).tail = p.

LaTeX

$$$ (p.cons x hx).tail = p $$$

Lean4

@[simp]
theorem tail_cons (p : RelSeries r) (x : α) (hx : x ~[r] p.head) : (p.cons x hx).tail (by simp) = p :=
  by
  apply toList_injective
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru