Theorems · Inductive type · order theory

BoundedOrderHom

(α : Type u_6) →
  (β : Type u_7) →
    [inst : Preorder α] → [inst_1 : Preorder β] → [BoundedOrder α] → [BoundedOrder β] → Type (max u_6 u_7)

The type of bounded order homomorphisms from α to β.

Defined in

Mathlib.Order.Hom.Bounded

Cited by

54 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

PreorderPreorderBoundedOrderBoundedOrder