Theorems · Definition · general topology

Polynomial.toContinuousMapOnAlgHom

{R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : TopologicalSpace R] → [inst_2 : IsTopologicalSemiring R] → (X : Set R) → Polynomial R →ₐ[R] C(↑X, R)

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

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

14 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceIsTopologicalSemiring