differentiableWithinAt — Mathlib

English

If f is differentiable at x, then f is differentiable within any set s at x; i.e., DifferentiableWithinAt 𝕜 f s x holds whenever DifferentiableAt 𝕜 f x holds.

Русский

Если f дифференцируема в точке x, то она дифференцируема внутри любого множества s в точке x.

LaTeX

$$$\\text{DifferentiableWithinAt}_{𝕜}(f,s,x) \\\\text{ holds whenever } \\text{DifferentiableAt}_{𝕜}(f,x).$$$

Lean4

protected theorem differentiableWithinAt : DifferentiableWithinAt 𝕜 f s x :=
  f.differentiableAt.differentiableWithinAt

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