# mathlibdocumentation

topology.continuous_function.polynomial

# Constructions relating polynomial functions and continuous functions. #

## Main definitions #

• polynomial.to_continuous_map_on p X: for X : set R, interprets a polynomial p as a bundled continuous function in C(X, R).
• polynomial.to_continuous_map_on_alg_hom: the same, as an R-algebra homomorphism.
• polynomial_functions (X : set R) : subalgebra R C(X, R): polynomial functions as a subalgebra.
• polynomial_functions_separates_points (X : set R) : (polynomial_functions X).separates_points: the polynomial functions separate points.
def polynomial.to_continuous_map {R : Type u_1} [semiring R] (p : polynomial R) :
C(R, R)

Every polynomial with coefficients in a topological semiring gives a (bundled) continuous function.

Equations
@[simp]
theorem polynomial.to_continuous_map_apply {R : Type u_1} [semiring R] (p : polynomial R) (x : R) :
@[simp]
theorem polynomial.to_continuous_map_on_apply {R : Type u_1} [semiring R] (p : polynomial R) (X : set R) (x : X) :
def polynomial.to_continuous_map_on {R : Type u_1} [semiring R] (p : polynomial R) (X : set R) :

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. [0,1].)

Equations
@[simp]
theorem polynomial.aeval_continuous_map_apply {R : Type u_1} {α : Type u_2} (g : polynomial R) (f : C(α, R)) (x : α) :

The algebra map from polynomial R to continuous functions C(R, R).

Equations
@[simp]
theorem polynomial.to_continuous_map_alg_hom_apply {R : Type u_1} (p : polynomial R) :
def polynomial.to_continuous_map_on_alg_hom {R : Type u_1} (X : set R) :

The algebra map from polynomial R to continuous functions C(X, R), for any subset X of R.

Equations
@[simp]
theorem polynomial.to_continuous_map_on_alg_hom_apply {R : Type u_1} (X : set R) (p : polynomial R) :
noncomputable def polynomial_functions {R : Type u_1} (X : set R) :

The subalgebra of polynomial functions in C(X, R), for X a subset of some topological semiring R.

Equations
@[simp]
theorem polynomial_functions_coe {R : Type u_1} (X : set R) :
theorem polynomial_functions_separates_points {R : Type u_1} (X : set R) :

The preimage of polynomials on [0,1] under the pullback map by x ↦ (b-a) * x + a is the polynomials on [a,b].