head_take

Mathlib.Order.RelSeries

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

English

The head of the prefix taken from p is the head of p.

Русский

Голова префикса, взятого из p, равна голове p.

LaTeX

$$$$ (\\mathrm{take}(p,i)).\\text{head} = p.\\text{head}. $$$$

Lean4

@[simp]
theorem head_take (p : RelSeries r) (i : Fin (p.length + 1)) : (p.take i).head = p.head := by simp [take, head]

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

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

Разделы

Аффилиация

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