differentiableAt — Mathlib

English

If HasDerivAt holds at x, then HasDerivWithinAt holds for any set s at x.

Русский

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

LaTeX

$$$\text{HasDerivAt } f\; f'\; x \Rightarrow \text{HasDerivWithinAt } f\; f'\; s\; x$$$

Lean4

theorem differentiableAt (h : HasDerivAt f f' x) : DifferentiableAt 𝕜 f x :=
  HasFDerivAt.differentiableAt h

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