English
We say that g is an order right adjoint of f if for every y, the set {x | f x ≤ y} has g y as its least upper bound.
Русский
Говорят, что g — правая сопряжённость к f, если для каждого y множество {x | f x ≤ y} имеет g y в качестве наименьшего верхнего границы.
LaTeX
$$$\\forall y,\\ IsLUB\\{x\\mid f x \\le y\\}(g y).$$$
Lean4
/-- 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. -/
def IsOrderRightAdjoint [Preorder α] [Preorder β] (f : α → β) (g : β → α) :=
∀ y, IsLUB {x | f x ≤ y} (g y)
