Theorems · Theorem · field theory

Polynomial.continuousWithinAt

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

Defined in

Mathlib.Topology.Algebra.Polynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceIsTopologicalSemiring