eval_polynomial — Mathlib

English

Same as EvalPolynomialAnalytic: taking polynomial evaluation of analytic function yields analytic within the same neighborhood.

Русский

То же самое, что EvalPolynomialAnalytic: оценка полинома по аналитической функции сохраняет аналитичность в той же окрестности.

LaTeX

$$AnalyticOnNhd\, 𝕜\, f\, s \Rightarrow AnalyticOnNhd\, 𝕜\, (Polynomial.eval · p) \; s$$

Lean4

theorem eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) : AnalyticOnNhd 𝕜 (eval · p) Set.univ :=
  analyticOnNhd_id.aeval_polynomial p

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