English
If two derivatives f0' and f1' both satisfy HasFDerivAt f f' x, then f0' = f1'.
Русский
Если две производные совпадают как производная функции f в точке x, то они равны между собой.
LaTeX
$$$ \\text{HasFDerivAt } f\\ f_0'\\ x \\;\\&\\; \\text{HasFDerivAt } f\\ f_1'\\ x \\Rightarrow f_0' = f_1'. $$$
Lean4
/-- Directional derivative agrees with `HasFDeriv`. -/
theorem lim (hf : HasFDerivAt f f' x) (v : E) {α : Type*} {c : α → 𝕜} {l : Filter α}
(hc : Tendsto (fun n => ‖c n‖) l atTop) : Tendsto (fun n => c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v)) :=
by
refine (hasFDerivWithinAt_univ.2 hf).lim _ univ_mem hc ?_
intro U hU
refine (eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_
convert mem_of_mem_nhds hU
dsimp only
rw [← mul_smul, mul_inv_cancel₀ hy, one_smul]
