comp_of_eq — 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 \\land AnalyticAt 𝕜 f x \\land f x = y \\Rightarrow AnalyticAt 𝕜 (g \\circ f) 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 𝕜 (g ∘ f) x := by
  rw [← hy] at hg
  exact hg.comp hf

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