head_cons

Mathlib.Order.RelSeries

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

English

The head of the new cons-predicted series equals the newHead.

Русский

Голова новой серии после добавления головы равна новой голове.

LaTeX

$$$ (p.cons newHead rel).head = newHead $$$

Lean4

@[simp]
theorem head_cons (p : RelSeries r) (newHead : α) (rel : newHead ~[r] p.head) : (p.cons newHead rel).head = newHead :=
  rfl

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

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

Разделы

Аффилиация

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