polynomial_comp_attachBound — Mathlib

English

For a subalgebra A of C(X,ℝ), f ∈ A and g ∈ ℝ[X], the postcomposition (g∘f).attachBound equals the aeval of g at f, i.e., (g.toContinuousMapOn Icc(−‖f‖,‖f‖)).comp f.attachBound = aeval(f) g.

Русский

Для подалгебры A ⊂ C(X,ℝ), f ∈ A и многочлена g ∈ ℝ[X], постсоставление g∘f после attachBound равно применения aeval к f:

LaTeX

$$$ (g^{\sim}\!\! , f) : (g\cdot f) = \mathrm{aeval}(f)(g)$$$

Lean4

theorem polynomial_comp_attachBound (A : Subalgebra ℝ C(X, ℝ)) (f : A) (g : ℝ[X]) :
    (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (f : C(X, ℝ)).attachBound = Polynomial.aeval f g :=
  by
  ext
  simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]
  simp

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