of_le — Mathlib

English

If a function f admits a finite power series expansion around a point x with order n, then for every larger order m ≥ n the same expansion also exists around x.

Русский

Если функция f имеет конечное разложение в виде ряда степенных вокруг точки x порядка n, то для любого большего порядка m ≥ n такое разложение существует вокруг x.

LaTeX

$$$\forall m,n\in\mathbb{N},\ HasFiniteFPowerSeriesAt\ f\ p\ x\ n \Rightarrow (n \le m) \Rightarrow HasFiniteFPowerSeriesAt\ f\ p\ x\ m.$$$

Lean4

theorem of_le {m n : ℕ} (h : HasFiniteFPowerSeriesAt f p x n) (hmn : n ≤ m) : HasFiniteFPowerSeriesAt f p x m :=
  by
  rcases h with ⟨r, hr⟩
  exact ⟨r, hr.of_le hmn⟩

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