continuous_aeval

Mathlib.Topology.Algebra.Polynomial

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

English

The map x ↦ aeval x p is continuous, when p is a polynomial and the base ring is appropriate.

Русский

Отображение x ↦ aeval x p непрерывно при надлежащих условиях на основание.

LaTeX

$$$\\forall p:\\, R[X], \\; Continuous(\\lambda x. aeval x p)$$$

Lean4

@[continuity, fun_prop]
protected theorem continuous_aeval : Continuous fun x : A => aeval x p :=
  p.continuous_eval₂ _

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

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

Разделы

Аффилиация

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