English
For any β with a preorder, and any fixed b in β, the constant map α → o β sending every input to b is an order-preserving map, i.e., an OrderHom β (OrderHom α β).
Русский
Для любого типа β с предоряжением и фиксированного b из β константное отображение α → o β, отправляющее каждый элемент в b, является монотонным отображением, то есть OrderHom β (OrderHom α β).
LaTeX
$$$ \text{const } (α)\, b : α \to^o β. $$$
Lean4
/-- Constant function bundled as an `OrderHom`. -/
@[simps -fullyApplied]
def const (α : Type*) [Preorder α] {β : Type*} [Preorder β] : β →o α →o β
where
toFun b := ⟨Function.const α b, fun _ _ _ => le_rfl⟩
monotone' _ _ h _ := h
