toLex_le_toLex — Mathlib

English

For elements a,b of Sum.Lex (i.e., the lex-ordered sum), the relation a ≤ b is exactly the corresponding Lex-ordered comparison of their representations via ofLex and toLex.

Русский

Для элементов из Sum.Lex отношение ≤ совпадает с лексикографическим сравнением их образов через ofLex и toLex.

LaTeX

$$$a \le b \iff \text{Lex.le} (\mathrm{toLex}\; a) (\mathrm{toLex}\; b).$$$

Lean4

@[simp]
theorem toLex_le_toLex [LE α] [LE β] {a b : α ⊕ β} : toLex a ≤ toLex b ↔ Lex (· ≤ ·) (· ≤ ·) a b :=
  Iff.rfl

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