comp_analyticWithinAt — Mathlib

English

If g is analytic at y and f is analytic at x, and f x = y, then g ∘ f is analytic at x.

Русский

Если g аналитична в y и f аналитична в x и f x = y, то g ∘ f аналитична в x.

LaTeX

$$$AnalyticAt 𝕜 g y → AnalyticAt 𝕜 f x → Eq (f x) y → AnalyticAt 𝕜 (g ∘ f) x$$$

Lean4

theorem comp_analyticWithinAt {g : F → G} {f : E → F} {x : E} {s : Set E} (hg : AnalyticAt 𝕜 g (f x))
    (hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithinAt 𝕜 (g ∘ f) s x :=
  by
  rw [← analyticWithinAt_univ] at hg
  exact hg.comp hf (Set.mapsTo_univ _ _)

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