ofHom — Mathlib

English

Typecheck a BoundedOrderHom as a morphism in BddOrd.

Русский

Типовой отображатель BoundOrderHom приводится к морфизму в BddOrd.

LaTeX

$$abbrev ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) : of X ⟶ of Y$$

Lean4

/-- Typecheck a `BoundedOrderHom` as a morphism in `BddOrd`. -/
abbrev ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y]
    (f : BoundedOrderHom X Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := BddOrd) f

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