comp_analyticOn — Mathlib

English

If f is analytic on s and g analytic on t, and g maps s into t, then g ∘ f is analytic on s.

Русский

Если f аналитичен на s, а g — аналитичен на t, и g(s) ⊆ t, то g ∘ f аналитична на s.

LaTeX

$$$AnalyticOnNhd 𝕜 f s \\to AnalyticOnNhd 𝕜 g t \\to Set.MapsTo g s t \\to AnalyticOnNhd 𝕜 (g \\circ f) s$$$

Lean4

theorem comp_analyticOn {f : F → G} {g : E → F} {s : Set F} {t : Set E} (hf : AnalyticOnNhd 𝕜 f s)
    (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) : AnalyticOn 𝕜 (f ∘ g) t := fun x m ↦
  (hf _ (h m)).comp_analyticWithinAt (hg x m)

Похожие утверждения