orderTop — Mathlib

English

The lexicographic top of a sum is the top of the right component.

Русский

Лексикографическая верхняя граница суммы — верхняя граница справа.

LaTeX

$$$\\text{OrderTop}(\\alpha \\oplus_ℓ \\beta)$ with top = inr ⊤$$

Lean4

/-- The lexicographical top of a sum is the top of the right component. -/
instance orderTop [LE α] [LE β] [OrderTop β] : OrderTop (α ⊕ₗ β)
    where
  top := inr ⊤
  le_top := by
    rintro (a | b)
    · exact Lex.sep _ _
    · exact Lex.inr le_top

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