continuous — Mathlib

English

For any polynomial p with coefficients in a topological ring R that is a topological semiring, the map x ↦ p.eval x is continuous.

Русский

Для любого многочлена p над кольцом R с топологией, образующаяся функция x ↦ p(x) непрерывна.

LaTeX

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

Lean4

@[continuity, fun_prop]
protected theorem continuous : Continuous fun x => p.eval x :=
  p.continuous_eval₂ _

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