get_strictMono

Mathlib.Data.List.NodupEquivFin

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

English

If l is strictly sorted by <, then l.get is strictly monotone.

Русский

Если список строго отсортирован по <, то функция get строго монотонна.

LaTeX

$$$ (\\text{Sorted}_{<}(l)) \\Rightarrow \\text{StrictMono}(l.{\\mathrm{get}}). $$$

Lean4

theorem get_strictMono (h : l.Sorted (· < ·)) : StrictMono l.get := fun _ _ => h.rel_get_of_lt

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

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

Разделы

Аффилиация

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