isOrderRightAdjoint_sSup — Mathlib

English

For any f: α→β, the map y ↦ sSup {x | f x ≤ y} is an order right adjoint to f.

Русский

Для любой f: α→β отображение y ↦ sSup {x | f x ≤ y} является правой смежной к f.

LaTeX

$$$\\text{IsOrderRightAdjoint } f \\ \\big( \\lambda y, \\mathrm{sSup}\\{x \\mid f x \\le y\\} \\big).$$$

Lean4

theorem isOrderRightAdjoint_sSup [CompleteSemilatticeSup α] [Preorder β] (f : α → β) :
    IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y} := fun _ => isLUB_sSup _

Похожие утверждения