Theorems · Theorem · real analysis

hasDerivAt_of_hasDerivAt_of_ne

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
  (∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) → ContinuousAt f x → ContinuousAt g x → HasDerivAt f (g x) x

If a real function f has a derivative g everywhere but at a point, and f and g are continuous at this point, then g is also the derivative of f at this point.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Extend

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace