comp_analyticWithinAt_of_eq — Mathlib

English

Version of the analytic composition rule with an equality hypothesis, stating that if hg g y, hf f x, and hy f x = y, then the composed function is analytic.

Русский

Версия правила аналитикaции композиции с предположением равенства; если hg g y, hf f x и hy: f x = y, то композиция аналитична.

LaTeX

$$$hg : AnalyticAt 𝕜 g y → hf : AnalyticAt 𝕜 f x → hy : f x = y → AnalyticAt 𝕜 (fun z => g (f z)) x$$$

Lean4

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

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