English
A corollary that there exists x' with the iterated derivative remainder form as above for Icc and Ioo intervals.
Русский
Следствие: существует точка x' с остатком в форме итеративной производной над интервалами Icc и Ioo.
LaTeX
$$$\\exists x' \\in Ioo(x_0,x), \\; f(x) - taylorWithinEval f n (Icc x_0 x) x_0 x = iteratedDerivWithin (n+1) f (Icc x_0 x) x' \\cdot \\frac{(x-x_0)^{n+1}}{(n+1)!}$$$
Lean4
theorem hasFDerivAt_of_tendstoLocallyUniformlyOn [NeBot l] {s : Set E} (hs : IsOpen s)
(hf' : TendstoLocallyUniformlyOn f' g' l s) (hf : ∀ n, ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x)
(hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasFDerivAt g (g' x) x :=
by
have h1 : s ∈ 𝓝 x := hs.mem_nhds hx
have h3 : Set.univ ×ˢ s ∈ l ×ˢ 𝓝 x := by simp only [h1, prod_mem_prod_iff, univ_mem, and_self_iff]
have h4 : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2 :=
eventually_of_mem h3 fun ⟨n, z⟩ ⟨_, hz⟩ => hf n z hz
refine hasFDerivAt_of_tendstoUniformlyOnFilter ?_ h4 (eventually_of_mem h1 hfg)
simpa [IsOpen.nhdsWithin_eq hs hx] using tendstoLocallyUniformlyOn_iff_filter.mp hf' x hx
