cpolynomialOn — Mathlib

English

If HasFiniteFPowerSeriesOnBall f p x n r, then the function f is continuously polynomial on the ball B(x,r).

Русский

Если имеет место HasFiniteFPowerSeriesOnBall для f и p, x, n, r, тогда f непрерывно полиноматична на шаре B(x,r).

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n r → CPolynomialOn 𝕜 f (EMetric.ball x r)$$

Lean4

theorem cpolynomialOn (hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialOn 𝕜 f (EMetric.ball x r) :=
  fun _y hy => hf.cpolynomialAt_of_mem hy

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