English
Let 𝕜 be a nontrivially normed field, and E, F, G be normed spaces. If f: F → G is analytic on a set s ⊆ F and g: E → F is analytic on t ⊆ E, and g maps t into s, then the composition f ∘ g is analytic on t.
Русский
Пусть 𝕜 — ненулевое нормированное поле, E, F, G — нормированные пространства. Если f: F → G аналитична на множестве s ⊆ F и g: E → F аналитичен на t ⊆ E, причём g(t) ⊆ s, то композиция f ∘ g аналитична на t.
LaTeX
$$$AnalyticOn 𝕜 f s \\land AnalyticOn 𝕜 g t \\land \\mathrm{MapsTo}~g~t~s \\Rightarrow AnalyticOn 𝕜 (f \\circ g) t$$$
Lean4
theorem comp {f : F → G} {g : E → F} {s : Set F} {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t)
(h : Set.MapsTo g t s) : AnalyticOn 𝕜 (f ∘ g) t := fun x m ↦ (hf _ (h m)).comp (hg x m) h
