head_toList

Mathlib.Order.RelSeries

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

English

For any p, the head of p.toList equals p.head provided toList is nonempty.

Русский

У головы p.toList равно p.head при условии непустого toList.

LaTeX

$$p.toList.head p.toList_ne_nil = p.head$$

Lean4

@[simp]
theorem head_toList (p : RelSeries r) : p.toList.head p.toList_ne_nil = p.head := by simp [toList, apply_zero]

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

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

Разделы

Аффилиация

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