get_mono

Mathlib.Data.List.NodupEquivFin

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

English

If l is sorted in nondecreasing order, then the function i ↦ l[i] is monotone.

Русский

Если список упорядочен неубывающе, то функция индексов к элементам списка монотонна.

LaTeX

$$$ (\\text{Sorted}_{\\le}(l)) \\Rightarrow \\operatorname{Monotone}(l.{\\mathrm{get}}). $$$

Lean4

theorem get_mono (h : l.Sorted (· ≤ ·)) : Monotone l.get := fun _ _ => h.rel_get_of_le

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

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

Разделы

Аффилиация

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