derivWithin_zero_of_isolated — Mathlib

English

If nhdsWithin x (s \\{x}) = ⊥, then derivWithin f s x = 0.

Русский

Если ненормированное окрестное пространство x в s без x равно ⊥, тогда derivWithin f s x = 0.

LaTeX

$$$\\bigl( \\mathrm{nhdsWithin}\\; x\\; (s \\setminus \\{x\\}) = \\bot \\bigr) \\Rightarrow \\ derivWithin\\,f\\,s\\,x = 0$$$

Lean4

@[deprecated derivWithin_zero_of_not_accPt (since := "2025-04-20")]
theorem derivWithin_zero_of_isolated (h : 𝓝[s \ { x }] x = ⊥) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_isolated h, ContinuousLinearMap.zero_apply]

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