Theorems · Definition · real analysis

deriv

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

Derivative of f at the point x, if it exists. Zero otherwise. If the derivative exists (i.e., ∃ f', HasDerivAt f f' x), then f x' = f x + (x' - x) • deriv f x + o(x' - x) where x' converges to x.

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

676 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpace