continuousOn

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#HasFiniteFPowerSeriesOnBall.continuousOn

← MathLib Explorer

English

Same as above with a different variable arrangement

Русский

То же самое с другой постановкой переменных

LaTeX

$$eq_partialSum' (hf) (y) (hy) (m) (hm) = ...$$

Lean4

/-- If a function admits a finite power series expansion on a disk, then it is continuous there. -/
protected theorem continuousOn (hf : HasFiniteFPowerSeriesOnBall f p x n r) : ContinuousOn f (EMetric.ball x r) :=
  hf.1.continuousOn

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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