derivWithin_zero_of_not_uniqueDiffWithinAt

English

If not UniqueDiffWithinAt 𝕜 s x, then derivWithin f s x = 0.

Русский

Если в точке x множество s не имеет уникальной точки дифференции, то derivWithin f s x = 0.

LaTeX

$$$\\neg \\operatorname{UniqueDiffWithinAt}_{\\mathbb{K}}(s,x) \\Rightarrow \\ derivWithin\\,f\\,s\\,x = 0.$$$

Lean4

theorem derivWithin_zero_of_not_uniqueDiffWithinAt (h : ¬UniqueDiffWithinAt 𝕜 s x) : derivWithin f s x = 0 :=
  derivWithin_zero_of_not_accPt <| mt AccPt.uniqueDiffWithinAt h

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