English
Let s be open and l a nontrivial filter. If f'_n → g' uniformly on l along s and for all n, HasDerivAt (f_n) (f'_n x) x, and f_n x → g x for all x in s, then g is differentiable at each x in s with derivative g'(x).
Русский
Пусть s открыто, l — не нулевой фильтр. Если производные f'_n сходятся равномерно к g' на l по s и для всех n функции f_n дифференцируемы в x с производной f'_n x, а f_n x сходится к g x для всех x ∈ s, тогда у g по каждому x ∈ s есть дифференциал g'(x).
LaTeX
$$$IsOpen(s) \to TendstoUniformlyOn f' g' l s \\to (\forallᶠ n in l, \forall x ∈ s, HasDerivAt (f n) (f' n x) x) \\to (\forall x ∈ s, Tendsto (fun n => f n x) l (\mathcal{N} (g x))) \\to \forall x ∈ s, HasDerivAt g (g' x) x$$$
Lean4
theorem hasDerivAt_of_tendstoUniformlyOn [NeBot l] {s : Set 𝕜} (hs : IsOpen s) (hf' : TendstoUniformlyOn f' g' l s)
(hf : ∀ᶠ n in l, ∀ x : 𝕜, x ∈ s → HasDerivAt (f n) (f' n x) x)
(hfg : ∀ x : 𝕜, x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasDerivAt g (g' x) x :=
hasDerivAt_of_tendstoLocallyUniformlyOn hs hf'.tendstoLocallyUniformlyOn hf hfg hx
