differentiableAt — Mathlib

English

If h is differentiable within s at x, then HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x.

Русский

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

LaTeX

$$$ \\text{DifferentiableWithinAt } 𝕜 f s x \\Rightarrow HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x. $$$

Lean4

theorem differentiableAt (h : DifferentiableWithinAt 𝕜 f s x) (hs : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
  h.imp fun _ hf' => hf'.hasFDerivAt hs

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