isOrderRightAdjoint_csSup — Mathlib

English

If α is conditionally complete and β is ordered, then the map f ↦ sSup {x | f x ≤ y} is an order right adjoint.

Русский

Если α — условно полноупорядоченная, а β — упорядоченная, то f ↦ sSup {x | f x ≤ y} образует правую сопряжённость.

LaTeX

$$$\\mathrm{isOrderRightAdjoint\_csSup} \ [ConditionallyCompleteLattice\\ α]\\ [Preorder\\ β] (f : α \\to β) : IsOrderRightAdjoint f (\\lambda y, \\mathrm{sSup} \\{x | f x ≤ y\\}).$$$

Lean4

theorem isOrderRightAdjoint_csSup [ConditionallyCompleteLattice α] [Preorder β] (f : α → β) (hne : ∀ y, ∃ x, f x ≤ y)
    (hbdd : ∀ y, BddAbove {x | f x ≤ y}) : IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y} := fun y =>
  isLUB_csSup (hne y) (hbdd y)

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