Theorems · Definition · real analysis

derivWithin

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

Derivative of f at the point x within the set s, if it exists. Zero otherwise. If the derivative exists (i.e., ∃ f', HasDerivWithinAt f f' s x), then f x' = f x + (x' - x) • derivWithin f s x + o(x' - x) where x' converges to x inside s.

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

258 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpace