hom — Mathlib

English

The morphism f: X ⟶ Y in LinOrd corresponds to the underlying order-preserving function on their carriers.

Русский

Гомоморфизм f: X ⟶ Y в LinOrd соответствует базовой функции, сохраняющей порядок, на картах X и Y.

LaTeX

$$$ (\mathrm{LinOrd.Hom.hom}(f))(x) = f(x). $$$

Lean4

/-- Turn a morphism in `LinOrd` back into a `OrderHom`. -/
abbrev hom {X Y : LinOrd.{u}} (f : Hom X Y) :=
  ConcreteCategory.hom (C := LinOrd) f

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