finite

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#HasFiniteFPowerSeriesAt.finite

English

If HasFiniteFPowerSeriesOnBall f p x n r holds, then for every m ≥ n, p_m = 0.

Русский

Если HasFiniteFPowerSeriesOnBall f p x n r выполняется, то для любого m ≥ n верно p_m = 0.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n r → ∀ m, n ≤ m → p_m = 0$$

Lean4

theorem finite (hf : HasFiniteFPowerSeriesAt f p x n) : ∀ m : ℕ, n ≤ m → p m = 0 :=
  let ⟨_, hf⟩ := hf;
  hf.finite

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

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

Разделы

Аффилиация

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