boundedOrder — Mathlib

English

The lexicographic order on Lex is a bounded order, combining the orderBot and orderTop from the components.

Русский

Лексикографический порядок образует ограниченный порядок, объединяя нижнюю и верхнюю границы компонент.

LaTeX

$$$\text{BoundedOrder}(\Sigma_\text{Lex} i, α(i))$ with \text{orderBot} and \text{orderTop}.$$

Lean4

/-- The lexicographical linear order on a sigma type. -/
instance boundedOrder [PartialOrder ι] [BoundedOrder ι] [∀ i, Preorder (α i)] [OrderBot (α ⊥)] [OrderTop (α ⊤)] :
    BoundedOrder (Σₗ i, α i) :=
  { Lex.orderBot, Lex.orderTop with }

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