orderTop — Mathlib

English

The lexicographic order on Σₗ' i, α i has a top element given by (⊤, ⊤), which is above every element of the sigma-type.

Русский

Лексикографический порядок на Σₗ' i, α_i имеет верхний элемент ⊤, который выше любого элемента сигма-типа.

LaTeX

$$$\\text{top} = (\\top,\\top)$ and ∀ x, x \\le_{\\mathrm{Lex}} \\text{top}$$$

Lean4

/-- The lexicographical linear order on a sigma type. -/
instance orderTop [PartialOrder ι] [OrderTop ι] [∀ i, Preorder (α i)] [OrderTop (α ⊤)] : OrderTop (Σₗ' i, α i)
    where
  top := ⟨⊤, ⊤⟩
  le_top := fun ⟨a, b⟩ => by
    obtain rfl | ha := eq_top_or_lt_top a
    · exact Lex.right _ le_top
    · exact Lex.left _ _ ha

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