tendsto_nhds — Mathlib

English

If a function has a Frechet derivative along a filter, then it tends to its derivative at the limit point.

Русский

Если у функции имеется производная Фреше вдоль фильтра, то она стремится к своей производной в предельной точке.

LaTeX

$$hasFDerivAtFilter f f' x L → Tendsto f L (nhds (f x))$$

Lean4

theorem tendsto_nhds (hL : L ≤ 𝓝 x) (h : HasFDerivAtFilter f f' x L) : Tendsto f L (𝓝 (f x)) :=
  by
  have : Tendsto (fun x' => f x' - f x) L (𝓝 0) :=
    by
    refine h.isBigO_sub.trans_tendsto (Tendsto.mono_left ?_ hL)
    rw [← sub_self x]
    exact tendsto_id.sub tendsto_const_nhds
  have := this.add (tendsto_const_nhds (x := f x))
  rw [zero_add (f x)] at this
  exact this.congr (by simp only [sub_add_cancel, forall_const])

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