polynomialFunctions.comap_compRightAlgHom_iccHomeoI

theorem polynomialFunctions.comap_compRightAlgHom_iccHomeoI : ∀ (a b : ℝ) (h : a < b), Subalgebra.comap (ContinuousMap.compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm.toContinuousMap) (polynomialFunctions unitInterval) = polynomialFunctions (Set.Icc a b)

This theorem states that the preimage of the set of polynomial functions defined on the interval `[0,1]` under the pullback map, which is defined by the function `x ↦ (b-a) * x + a`, is equal to the set of polynomial functions defined on the interval `[a,b]`. Here, `a` and `b` are any two real numbers such that `a < b`. The function `x ↦ (b-a) * x + a` is a homeomorphism from the interval `[a,b]` to `[0,1]`, and its inverse is used to define the pullback map. The set of polynomial functions on a subset of the real numbers is considered as a subalgebra of the algebra of continuous real-valued functions on that subset.

More concisely: The set of polynomial functions on the interval [`a, b`] is equal to the pullback under the homeomorphism `x mapsto (b-a) * x + a` of the set of polynomial functions on the interval [`0, 1`].