tail

Mathlib.Data.List.Chain

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

English

If l is an IsChain with respect to R, then its tail is also an IsChain with respect to R.

Русский

Если список является IsChain по отношению R, то его хвост тоже является IsChain по R.

LaTeX

$$IsChain R l → IsChain R l.tail$$

Lean4

theorem tail {l : List α} : IsChain R l → IsChain R l.tail := by induction l using twoStepInduction <;> grind

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

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

Разделы

Аффилиация

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