# Documentation

Mathlib.Topology.ContinuousFunction.Polynomial

# Constructions relating polynomial functions and continuous functions. #

## Main definitions #

• Polynomial.toContinuousMapOn p X: for X : Set R, interprets a polynomial p as a bundled continuous function in C(X, R).
• Polynomial.toContinuousMapOnAlgHom: the same, as an R-algebra homomorphism.
• 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.
@[simp]
theorem Polynomial.toContinuousMap_apply {R : Type u_1} [] [] (p : ) (x : R) :
=
def Polynomial.toContinuousMap {R : Type u_1} [] [] (p : ) :
C(R, R)

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

Instances For
@[simp]
theorem Polynomial.toContinuousMapOn_apply {R : Type u_1} [] [] (p : ) (X : Set R) (x : X) :
↑() x = ↑() x
def Polynomial.toContinuousMapOn {R : Type u_1} [] [] (p : ) (X : Set R) :
C(X, 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].)

Instances For
@[simp]
theorem Polynomial.aeval_continuousMap_apply {R : Type u_1} {α : Type u_2} [] [] [] (g : ) (f : C(α, R)) (x : α) :
↑(↑() g) x = Polynomial.eval (f x) g
@[simp]
theorem Polynomial.toContinuousMapAlgHom_apply {R : Type u_1} [] [] (p : ) :
Polynomial.toContinuousMapAlgHom p =

The algebra map from R[X] to continuous functions C(R, R).

Instances For
@[simp]
theorem Polynomial.toContinuousMapOnAlgHom_apply {R : Type u_1} [] [] (X : Set R) (p : ) :
def Polynomial.toContinuousMapOnAlgHom {R : Type u_1} [] [] (X : Set R) :
→ₐ[R] C(X, R)

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

Instances For
noncomputable def polynomialFunctions {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.

Instances For
@[simp]
theorem polynomialFunctions_coe {R : Type u_1} [] [] (X : Set R) :
theorem polynomialFunctions_separatesPoints {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].

theorem polynomialFunctions.eq_adjoin_X {R : Type u_1} [] [] (s : Set R) :