lt_def

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.Lex.lt_def

English

For any a,b in Sum.Lex, a < b is equivalent to the Lex LT comparison of their images under ofLex.

Русский

Для любых a,b из Sum.Lex верно: a < b эквивалентно LT-сравнению образов ofLex a и ofLex b.

LaTeX

$$$a < b \iff \text{Sum.Lex.LT.lt} (\mathrm{ofLex}\; a) (\mathrm{ofLex}\; b).$$$

Lean4

theorem lt_def [LT α] [LT β] {a b : α ⊕ₗ β} : a < b ↔ Lex (· < ·) (· < ·) (ofLex a) (ofLex b) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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