derivWithin_zero_of_notMem_closure

English

If H is a UniqueDiffWithinAt 𝕜 s x, and h, h1 are HasDerivWithinAt with possibly different derivatives f' and f1' on s at x, then f' = f1'.

Русский

Пусть H = UniqueDiffWithinAt 𝕜 s x; если существуют производные HasDerivWithinAt f f' s x и HasDerivWithinAt f f1' s x, то f' = f1'.

LaTeX

$$$\\text{UniqueDiffWithinAt}_{\\mathbb{K}}(s,x) \\Rightarrow \\Bigl( \\mathrm{HasDerivWithinAt}(f,f',s,x) \\wedge \\mathrm{HasDerivWithinAt}(f,f_1',s,x) \\Rightarrow f' = f_1' \\Bigr).$$$

Lean4

theorem derivWithin_zero_of_notMem_closure (h : x ∉ closure s) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]

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