toOrderHom — Mathlib

English

The order-preserving map underlying an order monoid homomorphism coincides with its order-hom representation.

Русский

Упорядоченное отображение, лежащее в основе OrderMonoidHom, совпадает с его представлением как OrderHom.

LaTeX

$$$((f : α →*o β) : α → o β) = f$$$

Lean4

/-- Reinterpret an ordered monoid homomorphism as an order homomorphism. -/
@[to_additive /-- Reinterpret an ordered additive monoid homomorphism as an order homomorphism. -/
    ]
def toOrderHom (f : α →*o β) : α →o β :=
  { f with }

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