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