English
The product-composition rule for analytic maps: if h is analytic on the product and f,g analytic on the domain, then x ↦ h(f(x), g(x)) is analytic on the domain.
Русский
правило аналитической композиции по умножению: если h аналитична на произведении, а f,g аналитичны на области, то x ↦ h(f(x), g(x)) аналитична на области.
LaTeX
$$$\\forall h:F\\times G\\to H,\\ f:E\\to F,\\ g:E\\to G,\\ s\\subseteq F\\times G,\\ t\\subseteq E,\\ (AnalyticOn 𝕜 h s) \\land (AnalyticOn 𝕜 f t) \\land (AnalyticOn 𝕜 g t) \\Rightarrow AnalyticOn 𝕜 (fun x \\mapsto h (f x, g x)) t$$$
Lean4
/-- `AnalyticOn.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} (ha : AnalyticOn 𝕜 h s)
(fa : AnalyticOn 𝕜 f t) (ga : AnalyticOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t := fun x hx ↦ (ha _ (m hx)).comp₂ (fa x hx) (ga x hx) m
