instOrdLexProd

Mathlib.Data.Prod.Lex

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

English

If α and β are orders, then the lexicographic order on α × β is an order (Ord).

Русский

Если α и β упорядочены, тогда лексикографический порядок на α × β является порядком (Ord).

LaTeX

$$$$ \text{instOrdLexProd}(\alpha, \beta) : \text{Ord}(\mathrm{Lex}(\alpha,\beta)). $$$$

Lean4

instance instOrdLexProd [Ord α] [Ord β] : Ord (α ×ₗ β) :=
  lexOrd

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

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

Разделы

Аффилиация

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