hasFDerivAt — Mathlib

English

If f is differentiable at x, then HasFDerivAt f (fderiv 𝕜 f x) x holds.

Русский

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

LaTeX

$$$DifferentiableAt\ 𝕜\ f\ x \Rightarrow\ HasFDerivAt\ f\ (fderiv\ 𝕜\ f\ x)\ x$$$

Lean4

theorem hasFDerivAt (h : DifferentiableAt 𝕜 f x) : HasFDerivAt f (fderiv 𝕜 f x) x :=
  by
  rw [fderiv, ← hasFDerivWithinAt_univ]
  rw [← differentiableWithinAt_univ] at h
  exact h.hasFDerivWithinAt

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