hasFTaylorSeriesUpTo_zero_iff — Mathlib

English

HasFTaylorSeriesUpTo 0 f p is equivalent to Continuous f and for all x, (p x 0).curry0 = f x.

Русский

HasFTaylorSeriesUpTo 0 f p эквивалентно непрерывности f и тому, что нулевой коэффициент ряда совпадает с f(x).

LaTeX

$$$\\text{HasFTaylorSeriesUpTo } 0\, f\, p \\;\\iff\\; \\text{Continuous } f \\wedge \\forall x, (p x 0).curry0 = f x$$

Lean4

theorem hasFTaylorSeriesUpTo_zero_iff : HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ x, (p x 0).curry0 = f x := by
  simp [hasFTaylorSeriesUpToOn_univ_iff.symm, continuousOn_univ, hasFTaylorSeriesUpToOn_zero_iff]

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