differentiableWithinAt — Mathlib

English

If HasFPowerSeriesWithinAt holds for f at x with s, then f is differentiable within insert x s at x.

Русский

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

LaTeX

$$$\text{HasFPowerSeriesWithinAt}(f,p,s,x) \Rightarrow \text{DifferentiableWithinAt}(f,\text{insert } x s, x)$$$

Lean4

theorem differentiableWithinAt (h : HasFPowerSeriesWithinAt f p s x) : DifferentiableWithinAt 𝕜 f (insert x s) x :=
  h.hasFDerivWithinAt.differentiableWithinAt

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