sSup_eq — Mathlib

English

For WithBot α, the supremum of a set S with no trivial bottom component and bounded above equals the embedding of the supremum of the preimage in α.

Русский

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

LaTeX

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

Lean4

theorem sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
    sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
  WithTop.sInf_eq (α := αᵒᵈ) hs h's

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