continuousAt

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#CPolynomialAt.continuousAt

English

A function that is polynomial on a set s is continuous on s in the subspace topology.

Русский

Функция, являющаяся полиномом на множествае s, непрерывна на s в подпространственной топологии.

LaTeX

$$CPolynomialOn 𝕜 f s → ContinuousOn f s$$

Lean4

protected theorem continuousAt (hf : CPolynomialAt 𝕜 f x) : ContinuousAt f x :=
  hf.analyticAt.continuousAt

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

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

Разделы

Аффилиация

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