tail

Mathlib.Data.List.Sort

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

← MathLib Explorer

English

The tail of a sorted list is sorted with the same relation.

Русский

Хвост отсортированного списка сохраняет ту же сортировку.

LaTeX

$$$\\forall r:\\alpha\\to\\alpha\\to\\text{Prop},\\; \\forall l:\\text{List}(\\alpha),\\; l.\\text{Sorted } r \\Rightarrow l.\\tail\\text{ Sorted } r$$$

Lean4

theorem tail {r : α → α → Prop} {l : List α} (h : Sorted r l) : Sorted r l.tail :=
  Pairwise.tail h

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

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

Разделы

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

Аффилиация

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