sInf_mem — Mathlib

English

If s is a nonempty compact subset in a suitable ordered topological space, then the infimum sInf s is actually an element of s.

Русский

Если s — непустое компактное множество в подходящем упорядоченном топологическом пространстве, то наименьшая верхняя грань sInf s принадлежит самому множеству.

LaTeX

$$$sInf\\,s \\in s$$$

Lean4

theorem sInf_mem [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : sInf s ∈ s :=
  let ⟨_a, ha⟩ := hs.exists_isLeast ne_s
  ha.csInf_mem

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