isGreatest_sSup — Mathlib

English

In the dual order, for a nonempty compact set s, the supremum behaves as a greatest lower bound in the dual space.

Русский

В двойственном порядке для непустого компактного множества s верхняя грань в исходном порядке становится GLB в двойственном порядке.

LaTeX

$$IsGLB(s, sInf s) in dual sense$$

Lean4

theorem isGreatest_sSup [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    IsGreatest s (sSup s) :=
  IsCompact.isLeast_sInf (α := αᵒᵈ) hs ne_s

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