theorem uniform_limit_derivative {f : ℕ → ℝ → ℝ} {g : ℝ → ℝ} {f' : ℕ → ℝ → ℝ} {lim : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hderiv : ∀ (n : ℕ), ∀ x ∈ Set.Icc a b, HasDerivAt (f n) (f' n x) x) (hf'_cont : ∀ (n : ℕ), ContinuousOn (f' n) (Set.Icc a b)) (hf'_unif : TendstoUniformlyOn f' g Filter.atTop (Set.Icc a b)) (hfg : ∀ x ∈ Set.Icc a b, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (lim x))) : (∀ x ∈ Set.Icc a b, HasDerivWithinAt lim (g x) (Set.Icc a b) x) ∧ ContinuousOn g (Set.Icc a b)

Interchange of limits and derivatives. Let f n : ℝ → ℝ be a sequence of functions on [a, b] such that each f n is differentiable on [a, b] with derivative f' n continuous on [a, b]. If f' n → g uniformly on [a, b] and f n x → lim x pointwise on [a, b], then the limit function lim is differentiable on [a, b] with derivative g, and g is continuous on [a, b]. In particular, this shows that the pointwise limit of a sequence of continuously differentiable functions whose derivatives converge uniformly is itself continuously differentiable, and that differentiation may be interchanged with the limit.