English
If HasFTaylorSeriesUpToOn n f p s and HasFTaylorSeriesUpToOn n g q s, then HasFTaylorSeriesUpToOn n (y ↦ (f y,g y)) (y ↦ (p y k).prod (q y k)) s.
Русский
Если f и g имеют ряды Тейлора p,q на s, то для пары (f,g) существует соответствующий ряд Тейлора, коэффициенты которого — произведения соответствующих коэффициентов p и q.
LaTeX
$$$ \HasFTaylorSeriesUpToOn_{\mathbb{K}}^{n} (f,g) \; s \;\to\; \HasFTaylorSeriesUpToOn_{\mathbb{K}}^{n} (y \mapsto (f y,g y)) (y \mapsto (p y k).prod (q y k)) s$$$
Lean4
/-- The composition of `C^n` functions on domains is `C^n`. -/
theorem comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s)
(st : MapsTo f s t) : ContDiffOn 𝕜 n (g ∘ f) s := fun x hx ↦ ContDiffWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st
