differentiableAt — Mathlib

English

If f is differentiable on s and x ∈ s has x ∈ neighborhood of s, then f is differentiable at x.

Русский

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

LaTeX

$$$DifferentiableOn\ 𝕜\ f\ s \land x \in s\Rightarrow\ DifferentiableAt\ 𝕜\ f\ x$$$

Lean4

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

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