hasFTaylorSeriesUpToOn_top_iff — Mathlib

English

If the order N is at least ∞, then HasFTaylorSeriesUpToOn N f p s is equivalent to HasFTaylorSeriesUpToOn n f p s for all finite n.

Русский

Если порядок N не меньше бесконечности, то HasFTaylorSeriesUpToOn N f p s эквивалентно HasFTaylorSeriesUpToOn n f p s для всех конечных n.

LaTeX

$$$$\text{HasFTaylorSeriesUpToOn}(N,f,p,s) \iff \forall n\in\mathbb{N}, \text{HasFTaylorSeriesUpToOn}(n,f,p,s).$$$$

Lean4

theorem hasFTaylorSeriesUpToOn_top_iff (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn n f p s := by
  simpa using hasFTaylorSeriesUpToOn_top_iff_add hN 0

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