Theorems · Definition · global analysis

taylorWithinEval

{E : Type u_2} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → ℕ → Set ℝ → ℝ → ℝ → E

The Taylor polynomial with derivatives inside of a set s considered as a function ℝ → E

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

27 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace