right_of_append

Mathlib.Data.List.Chain

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

English

If l1 ++ l2 is an IsChain, then l2 is an IsChain.

Русский

Если l1 ++ l2 образует IsChain, то l2 является IsChain.

LaTeX

$$IsChain R (instHAppendOfAppend.hAppend l1 l2) → IsChain R l2$$

Lean4

theorem right_of_append (h : IsChain R (l₁ ++ l₂)) : IsChain R l₂ :=
  (isChain_append.1 h).2.1

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

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

Разделы

Аффилиация

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