differentiableAt' — Mathlib

English

If a DiffContOnCl structure holds for a set, then at any point whose nhds intersects the set, the function is differentiable at that point.

Русский

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

LaTeX

$$$$\\text{If } h:\\ DiffContOnCl\\ 𝕜\\ f\\ s\\text{ and } nhds(x)\\cap s \\neq \\emptyset,\\ then } DifferentiableAt\\ 𝕜\\ f\\ x. $$$$

Lean4

theorem differentiableAt' (h : DiffContOnCl 𝕜 f s) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
  h.differentiableOn.differentiableAt hx

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