Theorems · Definition · global analysis

LineDifferentiableWithinAt

(𝕜 : 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 → Prop

f is line-differentiable at the point x in the direction v in the set s if there exists f' such that f (x + t v) = f x + t • f' + o (t) when t tends to 0 and x + t v ∈ s.

Defined in

Mathlib.Analysis.Calculus.LineDeriv.Basic

Cited by

19 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModule