mathlib documentation

topology.continuous_function.polynomial

Constructions relating polynomial functions and continuous functions. #

Main definitions #

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

Equations

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} [topological_space α] [comm_semiring R] [topological_space R] [topological_semiring R] (g : polynomial R) (f : C(α, R)) (x : α) :

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

Equations

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

Equations
noncomputable def polynomial_functions {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) :

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

Equations

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