Theorems · Definition · general topology

polynomialFunctions

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

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

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

16 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceIsTopologicalSemiring