eval_polynomial — Mathlib

English

Let p be a polynomial with coefficients in A. Then the map x ↦ p(x) from the normed space E to B is analytic on the entire space (i.e., on Set.univ).

Русский

Пусть p — полином с коэффициентами в A. Тогда отображение x ↦ p(x) из нормированного пространства E в B аналитично на всей области.

LaTeX

$$$\\forall p \\in A[X],\\quad \\text{AnalyticOn}_{\\mathbb{k}}(x \\mapsto \\operatorname{eval}(x,p))\\text{ на } E.$$$

Lean4

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

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