differentiableWithinAt — Mathlib

English

If f has a Fréchet derivative f' at x on s, then f is differentiable within s at x, i.e., differentiable on s in the sense of the internal derivative notion.

Русский

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

LaTeX

$$$$\\text{HasFDerivWithinAt } f\\,f'\\,s\\,x \\Rightarrow \\text{DifferentiableWithinAt } 𝕜 f\\,s\\,x.$$$$

Lean4

@[fun_prop]
theorem differentiableWithinAt (h : HasFDerivWithinAt f f' s x) : DifferentiableWithinAt 𝕜 f s x :=
  ⟨f', h⟩

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