Theorems · Definition · category theory

BddOrd.of

(X : Type u_1) → [inst : PartialOrder X] → [BoundedOrder X] → BddOrd

Construct a bundled BddOrd from the underlying type and typeclass.

Defined in

Mathlib.Order.Category.BddOrd

Cited by

9 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

PartialOrderBoundedOrder