le_def — Mathlib

English

For any a,b in Sum.Lex, a ≤ b is equivalent to applying the componentwise ≤ comparison to ofLex a and ofLex b.

Русский

Для любых элементов a,b из Sum.Lex верно: a ≤ b эквивалентно применению покомпонентному сравнению ≤ к ofLex a и ofLex b.

LaTeX

$$$a \le b \iff \text{Sum.Lex.LE.le} (\mathrm{ofLex}\; a) (\mathrm{ofLex}\; b).$$$

Lean4

theorem le_def [LE α] [LE β] {a b : α ⊕ₗ β} : a ≤ b ↔ Lex (· ≤ ·) (· ≤ ·) (ofLex a) (ofLex b) :=
  Iff.rfl

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