# mathlib3documentation

topology.continuous_function.polynomial

# Constructions relating polynomial functions and continuous functions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

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]
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 R[X] to continuous functions C(R, R).

Equations
@[simp]

The algebra map from R[X] 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].