instOrderTop — Mathlib

English

There is an OrderTop (top element) in the sInfHom type, defined by top := ⊤ and the obvious le_top property.

Русский

Для множества отображений sInfHom существует верхняя граница, задаваемая как константная функция, отправляющая все элементы в ⊤.

LaTeX

$$$\text{instance } \text{OrderTop } (sInfHom \alpha \beta) \text{ with } top := ⊤$$$

Lean4

instance : OrderTop (sInfHom α β) where
  top := ⊤
  le_top := fun _ _ => OrderTop.le_top _

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