theorem Real_Analysis.uniform_continuous_on_iff (f : ℝ → ℝ) (S : Set ℝ) : UniformContinuousOn f S ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ S, ∀ y ∈ S, |x - y| < δ → |f x - f y| < ε

A real function f is uniformly continuous on a set S ⊆ ℝ if and only if it satisfies the textbook ε–δ criterion: for every ε > 0 there exists δ > 0 such that |f x - f y| < ε for all x, y ∈ S with |x - y| < δ.