Theorems · Theorem · category theory

BddOrd.ofHom_apply

∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : BoundedOrder X] [inst_2 : PartialOrder Y] [inst_3 : BoundedOrder Y]
  (f : BoundedOrderHom X Y) (x : X), (CategoryTheory.ConcreteCategory.hom (BddOrd.ofHom f)) x = f x

Defined in

Mathlib.Order.Category.BddOrd

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms

Assumes

PartialOrderBoundedOrderPartialOrderBoundedOrder