Theorems · Definition · real analysis

HasDerivAtFilter

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

f has the derivative f' along the filter L. That is, f x' = f x + (x' - x) • f' + o(x' - x) where (x', x) converges along the filter L.

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

63 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousSMul