aeval_polynomial — Mathlib

English

If f is analytic at z and p is a polynomial, then the composition x ↦ aeval(f(x)) p defines an analytic function at z.

Русский

Если f аналитична в точке z и p — полином, то функция x ↦ aeval(f(x)) p аналитична в z.

LaTeX

$$$AnalyticAt\, 𝕜\, f\, z \Rightarrow AnalyticAt\, 𝕜\, (\lambda x. aeval (f x) p)\, z$$$

Lean4

theorem aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) : AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z :=
  by
  rw [← analyticWithinAt_univ] at hf ⊢
  exact hf.aeval_polynomial p

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