hasFTaylorSeriesUpTo_top_iff — Mathlib

English

For hN: ∞ ≤ N, HasFTaylorSeriesUpTo N f p is equivalent to HasFTaylorSeriesUpTo for all finite n after casting; i.e., HasFTaylorSeriesUpTo N f p ↔ ∀ n, HasFTaylorSeriesUpTo n.cast f p.

Русский

Для hN: ∞ ≤ N имеет место эквивалентность HasFTaylorSeriesUpTo N f p и HasFTaylorSeriesUpTo для всех конечных n после приведения типов.

LaTeX

$$$\\text{HasFTaylorSeriesUpTo } N f p \\;\\iff\\; \\forall n, \\text{HasFTaylorSeriesUpTo } n.cast\, f\, p$$

Lean4

theorem hasFTaylorSeriesUpTo_top_iff (hN : ∞ ≤ N) : HasFTaylorSeriesUpTo N f p ↔ ∀ n : ℕ, HasFTaylorSeriesUpTo n f p :=
  by simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff hN]

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