isChain_cons_iff_forall₂

Mathlib.Data.List.Chain

URI: https://scilib.ai/kg/mathlib#List.isChain_cons_iff_forall₂

English

IsChain R (a :: l) is equivalent to l = [] or Forall₂ R (a :: dropLast l) l.

Русский

IsChain R (a :: l) эквивалентно l = [] или Forall₂ R (a :: dropLast l) l.

LaTeX

$$$IsChain\\;R\\;(a :: l) \\iff l = [] \\lor Forall_2\\;R\\;(a :: l\\text{.dropLast})\\;l$$$

Lean4

theorem isChain_cons_iff_forall₂ : IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: dropLast l) l := by
  cases l <;> simp [isChain_iff_forall₂]

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

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

Разделы

Аффилиация

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