Convergence of slopes in topological modules

For a function with a derivative along a filter at a fixed base point, its slopes converge to that derivative after removing the base point from the filter. This applies to topological modules, including seminormed spaces where distinct points can have zero distance, and supplies the difference-quotient limit used to identify metric speed with the norm of a derivative.

theorem HasDerivAtFilter.tendsto_slope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [SeparatelyContinuousAdd E] [ContinuousSMul 𝕜 E] {γ : 𝕜 → E} {v : E} {t : 𝕜} {L : Filter 𝕜} (h : HasDerivAtFilter γ v (L ×ˢ pure t)) : Filter.Tendsto (slope γ t) (L ⊓ Filter.principal {t}ᶜ) (nhds v)

The slopes of a function with a derivative along a filter converge to that derivative away from the base point.