instTransOrdLex

Mathlib.Data.Prod.Lex

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

English

If α and β are ordered with transitivity, then Std.TransOrd holds for Lex(α × β).

Русский

Если α и β упорядочены с транзитивностью, то Std.TransOrd выполняется для Lex(α × β).

LaTeX

$$$$ \text{Std.TransOrd}(\mathrm{Lex}(\alpha,\beta)). $$$$

Lean4

instance [Ord α] [Ord β] [Std.TransOrd α] [Std.TransOrd β] : Std.TransOrd (α ×ₗ β) :=
  inferInstanceAs (Std.TransCmp (compareLex _ _))

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

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

Разделы

Аффилиация

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