English
The underlying set of polynomialFunctions X equals the range of the algebra hom from polynomials to continuous maps on X: (polynomialFunctions X : Set C(X,R)) = Set.range (toContinuousMapOnAlgHom X).
Русский
Функциональная подмножество polynomialFunctions X совпадает с образом алгебра-гомоморфизма от R[X] в C(X,R): (polynomialFunctions X : Set C(X,R)) = Set.range (toContinuousMapOnAlgHom X).
LaTeX
$$$ (polynomialFunctions X : Set C(X,R)) = Set.range (toContinuousMapOnAlgHom X) $$$
Lean4
@[simp]
theorem polynomialFunctions_coe (X : Set R) :
(polynomialFunctions X : Set C(X, R)) = Set.range (Polynomial.toContinuousMapOnAlgHom X) :=
by
ext
simp [polynomialFunctions]
-- TODO:
-- if `f : R → R` is an affine equivalence, then pulling back along `f`
-- induces a normed algebra isomorphism between `polynomialFunctions X` and
-- `polynomialFunctions (f ⁻¹' X)`, intertwining the pullback along `f` of `C(R, R)` to itself.
