toLex_mono

Mathlib.Data.Prod.Lex

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

English

The embedding toLex is strictly monotone: if x < y then toLex(x) < toLex(y).

Русский

Встраивание toLex strictly monotone: если x < y, то toLex(x) < toLex(y).

LaTeX

$$$$ x < y \Rightarrow \mathrm{toLex}(x) < \mathrm{toLex}(y). $$$$

Lean4

theorem toLex_mono : Monotone (toLex : α × β → α ×ₗ β) := fun _x _y hxy ↦ toLex_le_toLex'.2 ⟨hxy.1, fun _ ↦ hxy.2⟩

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

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

Разделы

Аффилиация

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