fderivWithin_zero_of_isolated — Mathlib

English

If the nhdsWithin x (s \ {x}) equals bottom, then fderivWithin 𝕜 f s x = 0.

Русский

Если nhdsWithin x (s без {x}) равен ⊥, то fderivWithin 𝕜 f s x = 0.

LaTeX

$$$\,nhdsWithin\ x\ (s \ {x}) = \bot \;\Rightarrow\; fderivWithin\ 𝕜\ f\ s\ x = 0$$$

Lean4

@[deprecated fderivWithin_zero_of_not_accPt (since := "2025-04-20")]
theorem fderivWithin_zero_of_isolated (h : 𝓝[s \ { x }] x = ⊥) : fderivWithin 𝕜 f s x = 0 := by
  rw [fderivWithin, if_pos (.of_nhdsWithin_eq_bot h)]

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