English
The Cartesian product of analytic functions is analytic when considered with the nhd (neighborhood) variant.
Русский
Картезианово произведение аналитических функций аналитично в варианте с окрестностями.
LaTeX
$$$\\forall h f g s t x,\\; (AnalyticOnNhd 𝕜 h s) \\land (AnalyticOnNhd 𝕜 f t) \\land (AnalyticOnNhd 𝕜 g t) \\Rightarrow AnalyticOnNhd 𝕜 (fun x \\mapsto h (f x, g x)) t$$$
Lean4
/-- `AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 h s)
(fa : AnalyticOnNhd 𝕜 f t) (ga : AnalyticOnNhd 𝕜 g t) (m : ∀ x, x ∈ t → (f x, g x) ∈ s) :
AnalyticOnNhd 𝕜 (fun x ↦ h (f x, g x)) t := fun _ xt ↦ (ha _ (m _ xt)).comp₂ (fa _ xt) (ga _ xt)
