hasFDerivAt — Mathlib

English

If f is differentiable on s and x lies in the neighborhood of s, then HasFDerivAt f (fderiv 𝕜 f x) x.

Русский

Если f дифференцируема на s и x лежит в окрестности s, то HasFDerivAt f (fderiv 𝕜 f x) x.

LaTeX

$$$DifferentiableOn\ 𝕜\ f\ s \to\ s \in 𝓝 x \Rightarrow\ HasFDerivAt\ f\ (fderiv\ 𝕜\ f\ x)\ x$$$

Lean4

theorem hasFDerivAt (h : DifferentiableOn 𝕜 f s) (hs : s ∈ 𝓝 x) : HasFDerivAt f (fderiv 𝕜 f x) x :=
  ((h x (mem_of_mem_nhds hs)).differentiableAt hs).hasFDerivAt

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