Continuous_Function_on_Closed_Interval_is_Uniformly_Continuous
Provedproofwikitopologyuniform-continuity
A continuous function on a closed bounded interval is uniformly continuous.
Preamble
import Mathlib.Topology.UniformSpace.Compact
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.UniformSpace.Compact theorem Continuous_Function_on_Closed_Interval_is_Uniformly_Continuous (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : UniformContinuousOn f (Set.Icc a b) := by sorry
Source