hasDerivAt_iff_tendsto_slope_zero

English

For a linear order, HasDerivAt f f' x is equivalent to the two-sided slope tending to f'.

Русский

Для линейного порядка условие существования производной эквивалентно сходимости наклона слева и справа к f'.

LaTeX

$$$HasDerivAt f f' x \\iff Tendsto (slope f x) (\\mathcal{N}_{x}^{<}) (\\mathcal{N} f') \\wedge Tendsto (slope f x) (\\mathcal{N}_{x}^{>}) (\\mathcal{N} f')$$$

Lean4

theorem hasDerivAt_iff_tendsto_slope_zero :
    HasDerivAt f f' x ↔ Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f') :=
  by
  have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by
    simp [nhdsWithin, map_add_left_nhds_zero x, Filter.map_inf, add_right_injective x]
  simp [hasDerivAt_iff_tendsto_slope, this, slope, Function.comp_def]

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