prefix

Mathlib.Data.List.Chain

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

English

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

Русский

Если l1 является префиксом l и l — IsChain, тогда l1 — IsChain.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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