coeFnHom — Mathlib

English

There is a forgetful functor from order-preserving maps to ordinary functions that simply takes the underlying function; this is monotone.

Русский

Существует забывающий функтор из монотонных отображений в обычные функции, который просто берет базовую функцию; он монотонен.

LaTeX

$$$ \mathrm{coeFnHom} : (α \to^o β) \to^o α \to β, \; \mathrm{coeFnHom}(f)=f. $$$

Lean4

/-- The "forgetful functor" from `α →o β` to `α → β` that takes the underlying function,
is monotone. -/
@[simps -fullyApplied]
def coeFnHom : (α →o β) →o α → β where
  toFun f := f
  monotone' _ _ h := h

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