differentiableWithinAt — Mathlib

English

If HasDerivWithinAt f f' s x holds, then f is differentiable within s at x.

Русский

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

LaTeX

$$$\text{HasDerivWithinAt } f\; f'\; s\; x \Longrightarrow \text{DifferentiableWithinAt } 𝕜\; f\; s\; x$$$

Lean4

theorem differentiableWithinAt (h : HasDerivWithinAt f f' s x) : DifferentiableWithinAt 𝕜 f s x :=
  HasFDerivWithinAt.differentiableWithinAt h

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