lean_workbook_plus_16403
ProvedSuppose that is such that for all for some . Prove that is uniformly continuous. Can be differentiable everywhere? Provide an example if not. Characterize the differentiability of in terms of integrability.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16403 (f : ℝ → ℝ) (c : ℝ) (hc : 0 < c) (h : ∀ x y, |f x - f y| ≤ c * |x - y|) : UniformContinuous f := by sorry
Source