LT — Mathlib · SciLib

English

The linear order on the Lexicographic sum is defined by Lex order on the components, i.e., Sum.Lex.LT is the lexicographic < on α ⊕ₗ β.

Русский

Линейный порядок на лексикографической сумме задан лексикографическим порядком по компонентам.

LaTeX

$$$\text{LT on }(\alpha \oplus_{\ell} \beta) = \text{Lex}((<)_{\alpha}, (<)_{\beta}).$$$

Lean4

/-- The linear/lexicographical `<` on a sum. -/
protected instance LT [LT α] [LT β] : LT (α ⊕ₗ β) :=
  ⟨Lex (· < ·) (· < ·)⟩

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