eq_zero_of_bound_zero — Mathlib

English

If a function admits a finite power series on a ball, then it is continuous on that ball.

Русский

Если функция имеет конечный степенной ряд на шаре, то она непрерывна на этом шаре.

LaTeX

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

Lean4

/-- If `f` has a formal power series on a ball bounded by `0`, then `f` is equal to `0` on
the ball. -/
theorem eq_zero_of_bound_zero (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) : ∀ y ∈ EMetric.ball x r, f y = 0 :=
  by
  intro y hy
  rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]
  simp only [Finset.range_zero, Finset.sum_empty]

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