continuous_eval₂ — Mathlib

English

For any polynomial p with coefficients in S and any ring hom f: S →+* R, the function x ↦ p.eval₂ f x is continuous.

Русский

Для любого многочлена p над S и кольцевого гомоморфизма f: S →+* R функция x ↦ p.eval₂ f x непрерывна.

LaTeX

$$$\\forall p \\in S[X], \\; f:S \\to+* R,\\; Continuous(\\lambda x. p.eval₂ f x)$$$

Lean4

@[continuity, fun_prop]
protected theorem continuous_eval₂ [Semiring S] (p : S[X]) (f : S →+* R) : Continuous fun x => p.eval₂ f x :=
  by
  simp only [eval₂_eq_sum]
  exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _)

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