rel_head

Mathlib.Data.List.Chain

URI: https://scilib.ai/kg/mathlib#List.IsChain.rel_head

English

If x, y, l form a chain x :: y :: l, then R x y holds.

Русский

Если последовательность x, y, l образует цепь, то выполняется R x y.

LaTeX

$$IsChain R (List.cons x (List.cons y l)) → R x y$$

Lean4

theorem rel_head {x y l} (h : IsChain R (x :: y :: l)) : R x y :=
  List.rel_of_isChain_cons_cons h

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

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

Разделы

Аффилиация

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