toList_getElem_zero_eq_head

Mathlib.Order.RelSeries

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

English

The 0-th element of toList equals the head.

Русский

Нулевой элемент toList равен head.

LaTeX

$$p.toList[0] = p.head$$

Lean4

@[simp]
theorem toList_getElem_zero_eq_head (p : RelSeries r) : p.toList[0] = p.head :=
  p.toList_getElem_eq_apply_of_lt_length (by simp)

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

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

Разделы

Аффилиация

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