comp — Mathlib

English

If g is analytic at f(x) and f is analytic at x, then the composition g ∘ f is analytic at x.

Русский

Если g аналитична в точке f(x), а f аналитична в x, тогда композиция g ∘ f аналитична в x.

LaTeX

$$$AnalyticAt 𝕜 g (f x) \\land AnalyticAt 𝕜 f x \\Rightarrow AnalyticAt 𝕜 (g \\circ f) x$$$

Lean4

/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
analytic at `x`. -/
@[fun_prop]
theorem comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) :
    AnalyticAt 𝕜 (g ∘ f) x := by
  rw [← analyticWithinAt_univ] at hg hf ⊢
  apply hg.comp hf (by simp)

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