Theorems · Definition · global analysis

lineDerivWithin

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → Set E → E → E → F

Line derivative of f at the point x in the direction v within the set s, if it exists. Zero otherwise. If the line derivative exists (i.e., ∃ f', HasLineDerivWithinAt 𝕜 f f' s x v), then f (x + t v) = f x + t lineDerivWithin 𝕜 f s x v + o (t) when t tends to 0 and x + t v ∈ s.

Defined in

Mathlib.Analysis.Calculus.LineDeriv.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModule