Theorems · Theorem · field theory

Polynomial.continuousAt

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) {a : R},
  ContinuousAt (fun x => Polynomial.eval x p) a

Defined in

Mathlib.Topology.Algebra.Polynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceIsTopologicalSemiring