English
If h is analytic at (f x, g x) and f, g analytic at x, then x ↦ h(f x, g x) is analytic at x.
Русский
Если h аналитична в точке (f(x), g(x)) и f, g аналитичны в x, то x ↦ h(f(x), g(x)) аналитична в x.
LaTeX
$$$\\forall h:F\\times G\\to H,\\ f:E\\to F,\\ g:E\\to G,\\ x:\\mathcal{E},\\ (AnalyticAt 𝕜 h { fst := f x, snd := g x }) \\land (AnalyticAt 𝕜 f x) \\land (AnalyticAt 𝕜 g x) \\Rightarrow AnalyticAt 𝕜 (fun x' \\mapsto h (f x', g x')) x$$$
Lean4
/-- `AnalyticAt.comp_analyticWithinAt` for functions on product spaces -/
theorem comp₂_analyticWithinAt {h : F × G → H} {f : E → F} {g : E → G} {x : E} {s : Set E}
(ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) :
AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) s x :=
AnalyticAt.comp_analyticWithinAt ha (fa.prod ga)
