bddAbove_image — Mathlib

English

If K is compact and f is continuous on K, then the image f[K] is bounded above.

Русский

Если K компактно, а f непрерывна на K, образ f[K] ограничен сверху.

LaTeX

$$BddAbove (f '' K)$$

Lean4

/-- A continuous function is bounded above on a compact set. -/
theorem bddAbove_image [ClosedIciTopology α] [Nonempty α] {f : β → α} {K : Set β} (hK : IsCompact K)
    (hf : ContinuousOn f K) : BddAbove (f '' K) :=
  IsCompact.bddBelow_image (α := αᵒᵈ) hK hf

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