continuousAt_div — Mathlib

English

If HasDerivAt f a c, then the update function x ↦ (f x − f c)/(x − c) is continuous at c.

Русский

Если существует производная HasDerivAt f a c, то отображение x ↦ (f x − f c)/(x − c) непрерывно в c.

LaTeX

$$$\\text{HasDerivAt } f a c \\Rightarrow \\text{ContinuousAt } (\\lambda x, (f x - f c)/(x-c)) c$$$

Lean4

theorem continuousAt_div [DecidableEq 𝕜] {f : 𝕜 → 𝕜} {c a : 𝕜} (hf : HasDerivAt f a c) :
    ContinuousAt (Function.update (fun x ↦ (f x - f c) / (x - c)) c a) c :=
  by
  rw [← slope_fun_def_field]
  exact continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

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