bddBelow_image — Mathlib

English

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

Русский

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

LaTeX

$$BddBelow (f '' K)$$

Lean4

/-- A continuous function is bounded below on a compact set. -/
theorem bddBelow_image [ClosedIicTopology α] [Nonempty α] {f : β → α} {K : Set β} (hK : IsCompact K)
    (hf : ContinuousOn f K) : BddBelow (f '' K) :=
  (hK.image_of_continuousOn hf).bddBelow

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