hasDerivAt — Mathlib

English

If f is differentiable on s and s is a neighborhood of x, then HasDerivAt f (deriv f x) x holds.

Русский

Если функция дифференцируема на множестве s и s содержит окрестность точки x, то имеет место производная в точке x равная deriv f x.

LaTeX

$$$\text{DifferentiableOn } 𝕜 f s \wedge s \in 𝓝 x \Rightarrow \text{HasDerivAt } f (deriv f x) x$$$

Lean4

theorem hasDerivAt (h : DifferentiableOn 𝕜 f s) (hs : s ∈ 𝓝 x) : HasDerivAt f (deriv f x) x :=
  (h.hasFDerivAt hs).hasDerivAt

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