toLex_le_toLex

Mathlib.Data.Prod.Lex

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

English

as above

Русский

как выше

LaTeX

$$$ x \\le_{lex} y \\iff \\dots $$$

Lean4

theorem toLex_le_toLex [LT α] [LE β] {x y : α × β} : toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.lex_def

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

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

Разделы

Аффилиация

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