differentiableAt — Mathlib

English

If a function is differentiable on a set, then it is differentiable at any point of that set that lies in its open interior.

Русский

Если функция дифференцируема на множестве, то она дифференцируема в любой точке множества, которая лежит внутри множества.

LaTeX

$$$$\\text{If } h:\\ DiffContOnCl\\ 𝕜\\ f\\ s\\text{ and } x\\in s^{\\circ},\\text{ then } DifferentiableAt\\ 𝕜\\ f\\ x. $$$$

Lean4

protected theorem differentiableAt (h : DiffContOnCl 𝕜 f s) (hs : IsOpen s) (hx : x ∈ s) : DifferentiableAt 𝕜 f x :=
  h.differentiableOn.differentiableAt <| hs.mem_nhds hx

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