ofHom — Mathlib

English

An order-homomorphism f: X →o Y can be regarded as a LinOrd morphism via ofHom f, acting by the same underlying function.

Русский

Гомоморфизм порядка f: X →o Y рассматривается как морфизм в LinOrd через ofHom f и действует той же функцией.

LaTeX

$$$ (\mathrm{ofHom}(f))(x) = f(x). $$$

Lean4

/-- Typecheck a `OrderHom` as a morphism in `LinOrd`. -/
abbrev ofHom {X Y : Type u} [LinearOrder X] [LinearOrder Y] (f : X →o Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := LinOrd) f

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