English
If h is HasFTaylorSeriesUpToOn n f p s and t ⊆ s, then h restricted to t remains HasFTaylorSeriesUpToOn n f p t.
Русский
Если h — HasFTaylorSeriesUpToOn n f p s и t ⊆ s, то на t сохраняется HasFTaylorSeriesUpToOn n f p t.
LaTeX
$$$HasFTaylorSeriesUpToOn\ n\ f\ p\ s \to t \subseteq s \Rightarrow HasFTaylorSeriesUpToOn n f p t$$$
Lean4
/-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
continuous. -/
theorem continuous_fderiv_apply (h : ContDiff 𝕜 n f) (hn : 1 ≤ n) :
Continuous fun p : E × E => (fderiv 𝕜 f p.1 : E → F) p.2 :=
have A : Continuous fun q : (E →L[𝕜] F) × E => q.1 q.2 := isBoundedBilinearMap_apply.continuous
have B : Continuous fun p : E × E => (fderiv 𝕜 f p.1, p.2) :=
((h.continuous_fderiv hn).comp continuous_fst).prodMk continuous_snd
A.comp B
