Theorems · Definition · real analysis

HasDerivAt

{𝕜 : 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. That is, f x' = f x + (x' - x) • f' + o(x' - x) where x' converges to x.

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

493 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousSMul