toOrderHom

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderHomClass.toOrderHom

← MathLib Explorer

English

For a : Regular α, toRegular (a : α) = a.

Русский

Для a : Regular α имеет место toRegular(a : α) = a.

LaTeX

$$$ toRegular((a : \alpha)) = a$$$

Lean4

/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` into an actual
`OrderHom`. This is declared as the default coercion from `F` to `α →o β`. -/
@[coe]
def toOrderHom (f : F) : α →o β where
  toFun := f
  monotone' := OrderHomClass.monotone f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru