continuousAt

Mathlib.Topology.Algebra.Polynomial

URI: https://scilib.ai/kg/mathlib#Polynomial.continuousAt

English

The evaluation map p ↦ p.eval is continuous at a given point a in A.

Русский

Отображение оценки многочлена непрерывно в точке a.

LaTeX

$$$\\forall p:\\, \\mathbb{R}[X], \\; \\text{ContinuousAt}(\\lambda x. p.eval x, a)$$$

Lean4

@[fun_prop]
protected theorem continuousAt {a : R} : ContinuousAt (fun x => p.eval x) a :=
  p.continuous.continuousAt

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru