exists_isGreatest — Mathlib

English

In a ClosedIciTopology, every compact nonempty set s has a greatest element.

Русский

В ClosedIciTopology любая компактная непустая множество имеет наибольший элемент.

LaTeX

$$IsCompact s → s.Nonempty → ∃ x ∈ s, IsGreatest s x$$

Lean4

theorem exists_isGreatest [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    ∃ x, IsGreatest s x :=
  IsCompact.exists_isLeast (α := αᵒᵈ) hs ne_s

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