Theorems · Theorem · real analysis

hasDerivWithinAt_Ici_of_tendsto_deriv

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E},
  DifferentiableOn ℝ f s →
    ContinuousWithinAt f s a →
      s ∈ nhdsWithin a (Set.Ioi a) →
        Filter.Tendsto (fun x => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds e) → HasDerivWithinAt f e (Set.Ici a) a

If a function is differentiable on the right of a point a : ℝ, continuous at a, and its derivative also converges at a, then f is differentiable on the right at a.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Extend

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace