lean_workbook_plus_76817

Proved

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

If $f$ and $g$ are uniformly continuous on $R$ , must $f o g$ (composition function $f(g(x))$ ) be uniformly continuous on $R$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76817 (f g : ℝ → ℝ) (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous (f ∘ g)   :=  by sorry

Source