eval_linearMap' — Mathlib

English

If f is a linear map with values in σ → B and p is a mvPolynomial, then the map x ↦ eval (f x) p is analytic on a neighborhood of every point.

Русский

Если f — линейное отображение сзначениями в σ → B, и p — mvPolynomial, то x ↦ eval (f x) p аналитично на окрестности в каждой точке.

LaTeX

$$$\\forall f:\\, E\\to \\sigma\\to B,\\; p:\\, MvPolynomial\\, \\sigma\\, B,\\ AnalyticOnNhd\\, 𝕜( x \\mapsto \\operatorname{eval}(f(x), p) )\\ Set.univ.$$$

Lean4

theorem eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) :
    AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ :=
  AnalyticOnNhd.eval_linearMap (.pi f) p

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