suffix

Mathlib.Data.List.Chain

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

English

If l is an IsChain and l1 is a suffix of l, then l1 is an IsChain.

Русский

Если l — IsChain, и l1 является суффиксом l, то l1 — IsChain.

LaTeX

$$IsChain R l → l1 <:+ l → IsChain R l1$$

Lean4

theorem suffix (h : IsChain R l) (h' : l₁ <:+ l) : IsChain R l₁ :=
  h.infix h'.isInfix

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

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

Разделы

Аффилиация

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