English
For analytic within-at on product spaces, the composition h(f, g) is analytic on t when f,g analytic on t and (f,g) maps t to s.
Русский
Для аналитичности внутри-на продуктовых пространствах композиция h(f,g) аналитична на t, если f и g аналитичны на t и (f,g) отображают t в s.
LaTeX
$$$\\forall h:F\\times G\\to H,\\ f:E\\to F,\\ g:E\\to G,\\ s\\subseteq F\\times G,\\ t\\subseteq E,\\ x\\in E,\\ (AnalyticWithinAt 𝕜 h s (f x, g x)) \\land (AnalyticWithinAt 𝕜 f t x) \\land (AnalyticWithinAt 𝕜 g t x) \\\\Rightarrow AnalyticWithinAt 𝕜 (fun x \\mapsto h (f x, g x)) t x$$$
Lean4
/-- `AnalyticWithinAt.comp` for functions on product spaces -/
theorem comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} {x : E}
(ha : AnalyticWithinAt 𝕜 h s (f x, g x)) (fa : AnalyticWithinAt 𝕜 f t x) (ga : AnalyticWithinAt 𝕜 g t x)
(hf : Set.MapsTo (fun y ↦ (f y, g y)) t s) : AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) t x :=
AnalyticWithinAt.comp ha (fa.prod ga) hf
