boundedOrder — Mathlib

English

The Lex-ordered sum of two bounded orders is a bounded order, with bottom given by inl ⊥ and top by inr ⊤.

Русский

Упорядоченная по лексикографическому правилу сумма двух ограниченных порядков образует ограниченный порядок; нуль слева, верх справа.

LaTeX

$$$\\text{BoundedOrder}(\\alpha \\oplus_ℓ \\beta)$$$

Lean4

instance boundedOrder [LE α] [LE β] [OrderBot α] [OrderTop β] : BoundedOrder (α ⊕ₗ β) :=
  { Lex.orderBot, Lex.orderTop with }

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