Theorems · Theorem · real analysis

HasFTaylorSeriesUpToOn.hasStrictFDerivAt

∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
  {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {n : WithTop ℕ∞} {s : Set E'}
  {f : E' → F'} {x : E'} {p : E' → FormalMultilinearSeries 𝕂 E' F'},
  HasFTaylorSeriesUpToOn n f p s →
    n ≠ 0 → s ∈ nhds x → HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x

If a function has a Taylor series at order at least 1, then at points in the interior of the domain of definition, the term of order 1 of this series is a strict derivative of f.

Defined in

Mathlib.Analysis.Calculus.ContDiff.RCLike

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace