English
Let h: F × G → H be analytic at (f(x), g(x)) and f, g be analytic at x. Then x ↦ h(f(x), g(x)) is analytic at x.
Русский
Пусть h: F × G → 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\\in E, \\\\ (AnalyticAt 𝕜 h (f x, g x)) \\land (AnalyticAt 𝕜 f x) \\land (AnalyticAt 𝕜 g x) \\Rightarrow AnalyticAt 𝕜 (fun x' \\mapsto h (f x', g x')) x$$$
Lean4
/-- `AnalyticAt.comp` for functions on product spaces -/
theorem comp₂ {h : F × G → H} {f : E → F} {g : E → G} {x : E} (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticAt 𝕜 f x)
(ga : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun x ↦ h (f x, g x)) x :=
AnalyticAt.comp ha (fa.prod ga)
