monotone_fst_ofLex

Mathlib.Data.Prod.Lex

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

English

The first projection from Lex(α × β) to α is monotone: if x ≤ y then fst(x) ≤ fst(y).

Русский

Первая проекция из Lex(α × β) на α монотонна: если x ≤ y, то fst(x) ≤ fst(y).

LaTeX

$$$$ x \le_{\mathrm{lex}} y \ \Rightarrow\ \mathrm{fst}(x) \le \mathrm{fst}(y). $$$$

Lean4

theorem monotone_fst_ofLex : Monotone fun x : α ×ₗ β ↦ (ofLex x).1 :=
  monotone_fst

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

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

Разделы

Аффилиация

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