sSup_eq — Mathlib

English

If top is not in S and S is bounded above, then the supremum of S in WithTop α equals the embedding of the supremum of the preimage of S in α.

Русский

Если ⊤ не принадлежит S и S ограничено сверху, то верхняя грань sSup S в WithTop α равна вложению верхней грани sSup предобраза S в α.

LaTeX

$$$$ \operatorname{sSup} S = \uparrow\bigl( \operatorname{sSup}\bigl( (\uparrow)^{-1} S \bigr) : \alpha \bigr) $$$$

Lean4

theorem sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) (hs' : BddAbove ((↑) ⁻¹' s : Set α)) :
    sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
  (if_neg hs).trans <| if_pos hs'

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