aeval_mvPolynomial — Mathlib

English

If for all i the mvPolynomial coordinates f · i are analytic on a neighborhood s, then the map x ↦ aeval(f(x)) p is analytic on s for any mvPolynomial p.

Русский

Если для всех i координаты mvPolynomial-функции f · i аналитичны на окрестности s, то отображение x ↦ aeval(f(x)) p аналитично на s для любого mvPolynomial p.

LaTeX

$$$\\bigl(\\forall i, AnalyticOnNhd\\,\\mathbb{k}(f\\cdot i)\\, s\\bigr) \\implies AnalyticOnNhd\\,\\mathbb{k}\\bigl( x \\mapsto \\operatorname{aeval}(f(x), p) \\bigr)\\, s.$$$

Lean4

theorem aeval_mvPolynomial (hf : ∀ i, AnalyticOnNhd 𝕜 (f · i) s) (p : MvPolynomial σ A) :
    AnalyticOnNhd 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p

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