rel_head?

Mathlib.Data.List.Chain

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

English

If IsChain R (x :: l) and head? l contains y, then R x y.

Русский

Если IsChain R (x :: l) и head? l содержит y, то R x y.

LaTeX

$$IsChain R (x :: l) → Option.instMembership.mem l.head? y → R x y$$

Lean4

theorem rel_head? {x l} (h : IsChain R (x :: l)) ⦃y⦄ (hy : y ∈ head? l) : R x y :=
  by
  rw [← cons_head?_tail hy] at h
  exact h.rel_head

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

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

Разделы

Аффилиация

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