Theorems · Definition · real analysis

HasStrictDerivAt

{𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] → [inst_3 : TopologicalSpace F] → [ContinuousSMul 𝕜 F] → (𝕜 → F) → F → 𝕜 → Prop

f has the derivative f' at the point x in the sense of strict differentiability. That is, f y - f z = (y - z) • f' + o(y - z) as y, z → x.

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

163 results in Mathlib

Foundations

Depth 105 from the axioms, rests on 2,423 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousSMul