isTerminalTop — Mathlib

English

In a preordered type, the top element is terminal in the associated category.

Русский

В порядке есть верхний элемент, который является терминальным объектом в соответствующей категории.

LaTeX

$$$ \\text{isTerminal}(\\top) \\text{ in the category associated to the preorder}. $$$

Lean4

/-- The greatest element of a preordered type is terminal in the category
associated to this preorder. -/
def isTerminalTop : IsTerminal (⊤ : C) :=
  IsTerminal.ofUnique _

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