bddAbove — Mathlib

English

A compact set is bounded above; by duality, the image of a continuous function on a compact set is likewise bounded above.

Русский

Компактное множество ограничено сверху; по дуалитету образ непрерывной функции на компактном множестве также ограничен сверху.

LaTeX

$$There exists b such that ∀ x ∈ S, x ≤ b.$$

Lean4

/-- A compact set is bounded above -/
theorem bddAbove [ClosedIciTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) : BddAbove s :=
  IsCompact.bddBelow (α := αᵒᵈ) hs

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