toLex_strictMono

Mathlib.Data.Sum.Order

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

English

Reiterates that the toLex map is strictly monotone as an order-preserving embedding.

Русский

Повторно утверждается, что отображение toLex строго монотонно как вложение в порядок.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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