orderTop — Mathlib

English

The evaluation of top for maps (order-preserving) is given by the constant function to the top element of β.

Русский

Для отображений порядка верхняя граница задаётся константной функций по верхнему элементу β.

LaTeX

$$$\text{top}_{\mathrm{OrderHom}(α,β)} = \mathrm{const}\; α\; \top_β$$$

Lean4

instance orderTop [Preorder β] [OrderTop β] : OrderTop (α →o β)
    where
  top := ⊤
  le_top _ _ := le_top

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