continuous_eval

Mathlib.Topology.Algebra.MvPolynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.continuous_eval

English

Evaluation map x ↦ eval x p is continuous for any polynomial p in MvPolynomial σ X.

Русский

Оценочная карта x ↦ eval x p непрерывна для любого многочлена p в MvPolynomial σ X.

LaTeX

$$Continuous (fun x => eval x p)$$

Lean4

theorem continuous_eval : Continuous fun x ↦ eval x p := by continuity

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

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

Разделы

Аффилиация

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