Image_of_Closed_Real_Interval_is_Bounded

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisproofwiki

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ . Then $f$ is bounded on $\closedint a b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Order.Basic

theorem Image_of_Closed_Real_Interval_is_Bounded (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : BddAbove (f '' Set.Icc a b) ∧ BddBelow (f '' Set.Icc a b) := by sorry

Source

https://proofwiki.org/wiki/Image_of_Closed_Real_Interval_is_Bounded

View graph