Theorems · Theorem · general topology

polynomialFunctions.comap_compRightAlgHom_iccHomeoI

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

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

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

1 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound