continuousAt_dslope_same — Mathlib

English

The slope dslope f a is continuous at a if and only if f is differentiable at a.

Русский

Поведение dslope f в точке a эквивалентно дифференцируемости f в точке a.

LaTeX

$$$\text{ContinuousAt}( dslope\ f\ a, a) \iff \text{DifferentiableAt} \ f\ a$$$

Lean4

@[simp]
theorem continuousAt_dslope_same : ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a := by
  simp only [dslope, continuousAt_update_same, ← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope]

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