fderivWithin_zero_of_notMem_closure

English

If x is not in closure s, then fderivWithin 𝕜 f s x = 0; this follows from the non-membership relative to closure.

Русский

Если x не принадлежит замыканию s, то fderivWithin 𝕜 f s x = 0; следует из того, что x не принадлежит closure.

LaTeX

$$$x \notin \overline{s} \Rightarrow fderivWithin\ 𝕜\ f\ s\ x = 0$$$

Lean4

theorem fderivWithin_zero_of_notMem_closure (h : x ∉ closure s) : fderivWithin 𝕜 f s x = 0 :=
  fderivWithin_zero_of_not_accPt (h ·.clusterPt.mem_closure)

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