norm_cderiv_sub_lt — Mathlib

English

If a sequence converges locally uniformly and the terms are differentiable on the domain, then derivatives converge locally uniformly as well.

Русский

Если последовательность сходится локально по униформности и члены дифференцируемы, то их производные сходятся локально по униформности.

LaTeX

$$$TendstoLocallyUniformlyOn\\ (\\mathrm{deriv} \\circ F)\\ (\\mathrm{deriv}\\ f)\\ p\\ U$$$

Lean4

theorem norm_cderiv_sub_lt (hr : 0 < r) (hfg : ∀ w ∈ sphere z r, ‖f w - g w‖ < M) (hf : ContinuousOn f (sphere z r))
    (hg : ContinuousOn g (sphere z r)) : ‖cderiv r f z - cderiv r g z‖ < M / r :=
  cderiv_sub hr hf hg ▸ norm_cderiv_lt hr hfg (hf.sub hg)

Похожие утверждения