Image_of_Interval_by_Continuous_Function_is_Interval

Proved

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

continuous-functionsproofwikireal-analysis

Let $I$ be a real interval. Let $f: I \to \R$ be a continuous real function. Then the image of $f$ is a real 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 Image_of_Interval_by_Continuous_Function_is_Interval (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : IsPreconnected (f '' Set.Icc a b) := by sorry

Source

https://proofwiki.org/wiki/Image_of_Interval_by_Continuous_Function_is_Interval

View graph