taylorWithinEval_self — Mathlib

English

Evaluating the Taylor polynomial at x0 yields f(x0) for every n by induction on n.

Русский

Оценка полинома Тейлора в точке x0 даёт f(x0) для любого n по индукции.

LaTeX

$$$taylorWithinEval\ f\ n\ s\ x_0\ x_0 = f\ x_0$$$

Lean4

/-- Evaluating the Taylor polynomial at `x = x₀` yields `f x`. -/
@[simp]
theorem taylorWithinEval_self (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) : taylorWithinEval f n s x₀ x₀ = f x₀ := by
  induction n with
  | zero => exact taylor_within_zero_eval _ _ _ _
  | succ k hk => simp [hk]

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