Theorems · Theorem · general topology

polynomialFunctions_coe

∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (X : Set R),
  ↑(polynomialFunctions X) = Set.range ⇑(Polynomial.toContinuousMapOnAlgHom X)

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceIsTopologicalSemiring