isChain_cons_append_singleton_iff_forall₂

Mathlib.Data.List.Chain

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

← MathLib Explorer

English

IsChain R (a :: l ++ [b]) is equivalent to Forall₂ R (a :: l) (l ++ [b]).

Русский

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

LaTeX

$$$IsChain\\;R\\;(a :: l ++ [b]) \\iff Forall_2\\;R\\;(a :: l)\\;(l ++ [b])$$$

Lean4

theorem isChain_cons_append_singleton_iff_forall₂ : IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b]) := by
  simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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