hasLineDerivAt_iff_tendsto_slope_zero

English

A more explicit form of HasLineDerivAt is given via a limit characterization of the slope, matching the one-sided/topology definitions for the line through x in direction v.

Русский

Более явная форма HasLineDerivAt выражается через предел скорости, соответствующий определению линейной производной вдоль прямой через x в направлении v.

LaTeX

$$$\text{HasLineDerivAt}_{\mathbb{k}}(f, f', x, v) \iff \lim_{t \to 0} \frac{f(x+t v)-f(x)}{t} = f' $$$

Lean4

theorem hasLineDerivAt_iff_tendsto_slope_zero :
    HasLineDerivAt 𝕜 f f' x v ↔ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f') := by
  simp only [HasLineDerivAt, hasDerivAt_iff_tendsto_slope_zero, zero_add, zero_smul, add_zero]

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