eval_continuousLinearMap' — Mathlib

English

Let f: E → σ → B be a continuous linear map-valued function and p a mvPolynomial in σ over B. Then the map x ↦ eval (f x) p is analytic on a neighborhood of every point.

Русский

Пусть f: E → σ → B — функция с непрерывно линейными значениями, и p — mvPolynomial над B. Тогда отображение x ↦ eval (f x) p аналитично в окрестности точек.

LaTeX

$$$\\forall p:\\, p\\in MvPolynomial\\,\\sigma\\, B,\\ \\ AnalyticOnNhd\\, 𝕜\\bigl( x \\mapsto \\operatorname{eval}(f(x), p) \\bigr)\\, \\{\\ast\\}.$$$

Lean4

theorem eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) :
    AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ := fun x _ ↦ .aeval_mvPolynomial (fun i ↦ (f i).analyticAt x) p

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