comp — Mathlib

English

If hg is analytic on g with t and hf analytic on f with s and st: maps from s to t, then the composition g ∘ f is analytic on s.

Русский

Если hg аналитична на g с областью t, hf аналитична на f с областью s, и st: MapsTo f s t, то g ∘ f аналитична на s.

LaTeX

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

Lean4

theorem comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : AnalyticOnNhd 𝕜 g t) (hf : AnalyticOnNhd 𝕜 f s)
    (st : Set.MapsTo f s t) : AnalyticOnNhd 𝕜 (g ∘ f) s :=
  comp' (mono hg (Set.mapsTo_iff_image_subset.mp st)) hf

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