taylor_within_zero_eval — Mathlib

English

The Taylor polynomial of order zero evaluates to the original function value at the base point: taylorWithinEval f 0 s x0 x = f x0.

Русский

Полином Тейлора нулевого порядка принимает значение функции в точке x0: taylorWithinEval f 0 s x0 x = f(x0).

LaTeX

$$$taylorWithinEval\ f\ 0\ s\ x_0\ x = f\ x_0$$$

Lean4

/-- The Taylor polynomial of order zero evaluates to `f x`. -/
@[simp]
theorem taylor_within_zero_eval (f : ℝ → E) (s : Set ℝ) (x₀ x : ℝ) : taylorWithinEval f 0 s x₀ x = f x₀ :=
  by
  dsimp only [taylorWithinEval]
  dsimp only [taylorWithin]
  dsimp only [taylorCoeffWithin]
  simp

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