lineDeriv — Mathlib

English

If two line derivatives coincide, then their values are equal; otherwise, no contradiction arises.

Русский

Если две линейные производные совпадают, их значения равны; иначе противоречий нет.

LaTeX

$$$$\forall f f' f'' x v,\ HasLineDerivAt 𝕜 f f' x v \land HasLineDerivAt 𝕜 f f'' x v \Rightarrow f' = f''.$$$$

Lean4

/-- Line derivative of `f` at the point `x` in the direction `v`, if it exists.  Zero otherwise.

If the line derivative exists (i.e., `∃ f', HasLineDerivAt 𝕜 f f' x v`), then
`f (x + t v) = f x + t lineDeriv 𝕜 f x v + o (t)` when `t` tends to `0`.
-/
def lineDeriv (f : E → F) (x : E) (v : E) : F :=
  deriv (fun t ↦ f (x + t • v)) (0 : 𝕜)

Похожие утверждения