derivWithin_zero_of_not_accPt — Mathlib

English

If x is not an accumulation point of s, then derivWithin f s x = 0.

Русский

Если x не является точкой накопления множества s, то derivWithin f s x = 0.

LaTeX

$$$\\bigl( \\neg \\operatorname{AccPt}(x,\\mathcal{P}s) \\bigr) \\Rightarrow \\ derivWithin\\,f\\,s\\,x = 0$$$

Lean4

theorem derivWithin_zero_of_not_accPt (h : ¬AccPt x (𝓟 s)) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]

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