comp' — Mathlib

English

If g is analytic on t with respect to the image of f and f is analytic on s, then g ∘ f is analytic on s.

Русский

Если g аналитична на t относительно образа f и f аналитична на s, то g ∘ f аналитична на s.

LaTeX

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

Lean4

/-- If two functions `g` and `f` are analytic respectively on `s.image f` and `s`, then `g ∘ f` is
analytic on `s`. -/
theorem comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOnNhd 𝕜 g (s.image f)) (hf : AnalyticOnNhd 𝕜 f s) :
    AnalyticOnNhd 𝕜 (g ∘ f) s := fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)

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