toLex_lt_toLex — Mathlib

English

For α, β with LT, the order relation on Sum.Lex corresponds to the Lex-ordered LT on a,b; i.e., toLex a < toLex b iff Lex.lt on a,b.

Русский

Для α, β с LT порядок на Sum.Lex соответствует лексикографическому LT; то есть toLex a < toLex b тогда и только тогда, когда a,b образуют лексическое сравнение LT.

LaTeX

$$$\mathrm{toLex} a < \mathrm{toLex} b \iff \text{Lex.lt} a b.$$$

Lean4

@[simp]
theorem toLex_lt_toLex [LT α] [LT β] {a b : α ⊕ β} : toLex a < toLex b ↔ Lex (· < ·) (· < ·) a b :=
  Iff.rfl

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