Theorems · Definition · general topology

Polynomial.toContinuousMapOn

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

A polynomial as a continuous function, with domain restricted to some subset of the semiring of coefficients. (This is particularly useful when restricting to compact sets, e.g. [0,1].)

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

9 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceIsTopologicalSemiring