English
Let F be a type of function-like objects α → β, and suppose α and β are preordered with bounded order structures, and F satisfies the appropriate bounded-order-homomorphism class. Then each element f ∈ F can be viewed as a bounded-order-homomorphism from α to β via a canonical construction toBoundedOrderHom(f): the underlying map is f, and it preserves both the top and bottom elements.
Русский
Пусть F — множество отображений α → β с надлежащей структурой; при этом α и β образуют упорядоченные множества с границами, и F удовлетворяет требуемому классу гомоморфизмов ограниченного порядка. Тогда любой элемент f ∈ F можно неявно рассматривать как гомоморфизм ограниченного порядка f̂ = toBoundedOrderHom(f): базовая функция равна f, и она сохраняет верхнюю и нижнюю границы.
LaTeX
$$$\\operatorname{toBoundedOrderHom}(f) : \\operatorname{BoundedOrderHom}(\\alpha,\\beta), \\quad (\\operatorname{toBoundedOrderHom}(f))(x)=f(x), \\quad (\\operatorname{toBoundedOrderHom}(f))(\\top_\\alpha)=\\top_\\beta, \\quad (\\operatorname{toBoundedOrderHom}(f))(\\bot_\\alpha)=\\bot_\\beta.$$$
Lean4
/-- Turn an element of a type `F` satisfying `BoundedOrderHomClass F α β` into an actual
`BoundedOrderHom`. This is declared as the default coercion from `F` to `BoundedOrderHom α β`. -/
@[coe]
def toBoundedOrderHom [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] (f : F) :
BoundedOrderHom α β :=
{ (f : α →o β) with toFun := f, map_top' := map_top f, map_bot' := map_bot f }
