of_le — Mathlib

English

If there is a finite F-power series on ball for some n, then it also holds for any m ≥ n.

Русский

Если для некоторого n существует конечный F-ряд на шаре, тогда такое же верно и для любого m ≥ n.

LaTeX

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

Lean4

theorem of_le {m n : ℕ} (h : HasFiniteFPowerSeriesOnBall f p x n r) (hmn : n ≤ m) :
    HasFiniteFPowerSeriesOnBall f p x m r :=
  ⟨h.toHasFPowerSeriesOnBall, fun i hi ↦ h.finite i (hmn.trans hi)⟩

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