English
Typecheck an OrderHom as a morphism in FinPartOrd: for any X, Y with PartialOrder and Finite, and f: X →o Y, there is a morphism of FinPartOrd given by ofHom f.
Русский
Типизирована карта OrderHom как морфизм в FinPartOrd: для любых X, Y с PartialOrder и Finite, и f: X →o Y существует морфизм FinPartOrd, задаваемый ofHom f.
LaTeX
$$$ \\mathrm{ofHom}\\{X,Y\\}\\; (f: X \\to_o Y) : \\mathrm{of}\; X \\to \\mathrm{of}\; Y $$$
Lean4
/-- Typecheck a `OrderHom` as a morphism in `FinPartOrd`. -/
abbrev ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) : of X ⟶ of Y :=
ConcreteCategory.ofHom (C := FinPartOrd) f
