toLex_mono

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.Lex.toLex_mono

English

The map toLex from α ⊕ β is strictly monotone, i.e., it preserves strict order.

Русский

Отображение toLex строго монотонно по отношению к порядку: если a < b, то toLex(a) < toLex(b).

LaTeX

$$$\\text{StrictMono}(\\,\\text{toLex}\\,)$$$

Lean4

theorem toLex_mono : Monotone (@toLex (α ⊕ β)) := fun _ _ h => h.lex

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

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

Разделы

Аффилиация

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