comp_of_eq' — Mathlib

English

If g is analytic at y and f is analytic at x, and f x = y, then the composed function z ↦ g(f z) is analytic at x.

Русский

Если g аналитична в y и f аналитична в x и f x = y, то z ↦ g(f z) аналитично в x.

LaTeX

$$$AnalyticAt 𝕜 g y \\land AnalyticAt 𝕜 f x \\land f x = y \\Rightarrow AnalyticAt 𝕜 (fun z => g (f z)) x$$$

Lean4

/-- Version of `AnalyticAt.comp` where point equality is a separate hypothesis. -/
theorem comp_of_eq' {g : F → G} {f : E → F} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y) (hf : AnalyticAt 𝕜 f x)
    (hy : f x = y) : AnalyticAt 𝕜 (fun z ↦ g (f z)) x := by apply hg.comp_of_eq hf hy

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