Theorems · Theorem · general topology

Polynomial.toContinuousMapOn_X_eq_restrict_id

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (s : Set R),
  Polynomial.X.toContinuousMapOn s = ContinuousMap.restrict s (ContinuousMap.id R)

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceIsTopologicalSemiring