instCoeTCBoundedOrderHomOfBoundedOrderHomClass

English

There is a canonical coercion from any f ∈ F to a BoundedOrderHom α β, given by toBoundedOrderHom(f). This yields a coercion structure CoeTC F (BoundedOrderHom α β).

Русский

Существуют канонические приведения из любого элемента f ∈ F к гомоморфизму ограниченного порядка α → β, заданные через toBoundedOrderHom(f). Это образует структуру приведения CoeTC F (BoundedOrderHom α β).

LaTeX

$$$\\iota: F \\to \\operatorname{BoundedOrderHom}(\\alpha,\\beta),\\quad \\iota(f)=\\operatorname{toBoundedOrderHom}(f).$$$

Lean4

instance [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
    CoeTC F (BoundedOrderHom α β) :=
  ⟨BoundedOrderHomClass.toBoundedOrderHom⟩

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