orderBot — Mathlib

English

The lexicographic bottom of a sum is the bottom of the left component.

Русский

Лексикографическая нулевая нижняя граница суммы равна нулю слева.

LaTeX

$$$\\text{OrderBot}(\\alpha \\oplus_ℓ \\beta)$ with bottom = inl ⊥$$

Lean4

/-- The lexicographical bottom of a sum is the bottom of the left component. -/
instance orderBot [LE α] [OrderBot α] [LE β] : OrderBot (α ⊕ₗ β)
    where
  bot := inl ⊥
  bot_le := by
    rintro (a | b)
    · exact Lex.inl bot_le
    · exact Lex.sep _ _

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