Theorems · Definition · global analysis

HasLineDerivWithinAt

(𝕜 : 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) → F → Set E → E → E → Prop

f has the derivative f' at the point x along the direction v in the set s. That is, f (x + t v) = f x + t • f' + o (t) when t tends to 0 and x + t v ∈ s. Note that this definition is less well behaved than the total Fréchet derivative, which should generally be favored over this one.

Defined in

Mathlib.Analysis.Calculus.LineDeriv.Basic

Cited by

22 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModule