Theorems · Theorem · global analysis

taylorWithinEval_self

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ),
  taylorWithinEval f n s x₀ x₀ = f x₀

Evaluating the Taylor polynomial at x = x₀ yields f x.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

7 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace