continuousWithinAt_aeval — Mathlib

English

For any p, the function x ↦ aeval x p is continuous within a set s at a.

Русский

Для любого p функция x ↦ aeval x p непрерывна внутри множества s в точке a.

LaTeX

$$$\\forall p, s, a,\\; ContinuousWithinAt(\\lambda x. AlgHom.funLike.coe (Polynomial.aeval x) p, s, a)$$$

Lean4

@[fun_prop]
protected theorem continuousWithinAt_aeval {s a} : ContinuousWithinAt (fun x : A => aeval x p) s a :=
  p.continuous_aeval.continuousWithinAt

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