aeval_polynomial — Mathlib

English

If f is analytic on a neighborhood, then for every polynomial p, the map x ↦ aeval (f(x)) p is analytic on that neighborhood.

Русский

Если f аналитична на окне, то для любого полинома p функция x ↦ aeval(f(x)) p аналитична на этом окне.

LaTeX

$$$AnalyticOnNhd\, 𝕜\, f\, s \;\Rightarrow\; AnalyticOnNhd\, 𝕜\, (\lambda x. AlgHom.funLike.coe (Polynomial.aeval (f x)) p)\, s$$$

Lean4

theorem aeval_polynomial (hf : AnalyticOn 𝕜 f s) (p : A[X]) : AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦
  (hf x hx).aeval_polynomial p

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