Constructions relating polynomial functions and continuous functions. #
Main definitions #
Polynomial.toContinuousMapOn p X: for
X : Set R, interprets a polynomial
pas a bundled continuous function in
Polynomial.toContinuousMapOnAlgHom: the same, as an
polynomialFunctions (X : Set R) : Subalgebra R C(X, R): polynomial functions as a subalgebra.
polynomialFunctions_separatesPoints (X : Set R) : (polynomialFunctions X).SeparatesPoints: the polynomial functions separate points.
A polynomial as a continuous function, with domain restricted to some subset of the semiring of coefficients.
(This is particularly useful when restricting to compact sets, e.g.
The preimage of polynomials on
[0,1] under the pullback map by
x ↦ (b-a) * x + a
is the polynomials on