instBoundedOrderHomClass — Mathlib

English

The collection of all bounded-order preserving maps from α to β, i.e., maps that preserve the order and map the top and bottom elements appropriately, forms a structure of homomorphisms (BoundedOrderHomClass) between α and β.

Русский

Обозначение множества всех отображений с сохранением упорядочения и отображения верхнего и нижнего пределов между α и β образует структуру гомоморфизмов ограниченного порядка.

LaTeX

$$$\{ f: \alpha \to \beta \;\mid\; f \text{ preserves } \le,\; f(\top_\alpha)=\top_\beta,\; f(\bot_\alpha)=\bot_\beta \}$.$$

Lean4

instance : BoundedOrderHomClass (BoundedOrderHom α β) α β
    where
  map_rel f := @(f.monotone')
  map_top f := f.map_top'
  map_bot f := f.map_bot'

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