LineDifferentiableWithinAt — Mathlib

English

In a one-dimensional setting, the line derivative along v at x is given by the derivative of the map t ↦ f(x + t v) at t = 0.

Русский

В одномерном случае линейная производная по направлению v в точке x равна производной по t у функции t ↦ f(x + t v) в t = 0.

LaTeX

$$$$\text{LineDifferentiableAt } f x v = \text{DifferentiableAt } 𝕜 (t \mapsto f(x + t v)) (0).$$$$

Lean4

/-- `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`.
-/
def LineDifferentiableWithinAt (f : E → F) (s : Set E) (x : E) (v : E) : Prop :=
  DifferentiableWithinAt 𝕜 (fun t ↦ f (x + t • v)) ((fun t ↦ x + t • v) ⁻¹' s) (0 : 𝕜)

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