fderivWithin_zero_of_not_accPt — Mathlib

English

If the derivative exists vacuously when x is not an accumulation point of s, then fderivWithin 𝕜 f s x = 0.

Русский

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

LaTeX

$$$\text{If } \AccPt x(\mathcal{P}s)\text{ is false, then } fderivWithin\ 𝕜\ f\ s\ x = 0.$$$

Lean4

theorem fderivWithin_zero_of_not_accPt (h : ¬AccPt x (𝓟 s)) : fderivWithin 𝕜 f s x = 0 := by
  rw [fderivWithin, if_pos (.of_not_accPt h)]

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