Theorems · Definition · order theory

IsOrderRightAdjoint

{α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Prop

We say that g : β → α is an order right adjoint function for f : α → β if it sends each y to a least upper bound for {x | f x ≤ y}. If α is a partial order, and f : α → β has a right adjoint, then this right adjoint is unique.

Defined in

Mathlib.Order.SemiconjSup

Cited by

7 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderPreorder