Continuous_Image_of_Closed_Interval_is_Closed_Interval

Proved

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

continuous-functionsproofwikireal-analysis

Let $f$ be a real function which is continuous on the closed interval $\left[{a \,.\,.\, b}\right]$ . Then the image of $\left[{a \,.\,.\, b}\right]$ under $f$ is also a closed interval.

Preamble

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

Formal statement

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

theorem Continuous_Image_of_Closed_Interval_is_Closed_Interval (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : ∃ c d : ℝ, c ≤ d ∧ f '' Set.Icc a b = Set.Icc c d := by sorry

Source

https://proofwiki.org/wiki/Continuous_Image_of_Closed_Interval_is_Closed_Interval

View graph