hasDerivWithinAt_diff_singleton — Mathlib

English

HasDerivWithinAt f f' (s \\ { x }) x is equivalent to HasDerivWithinAt f f' s x.

Русский

HasDerivWithinAt f f' с разностью s и {x} эквивалентно HasDerivWithinAt f f' s x.

LaTeX

$$$\\mathrm{HasDerivWithinAt}(f,f',\\,S\\setminus\\{x\\},x) \\iff \\mathrm{HasDerivWithinAt}(f,f',S,x).$$$

Lean4

@[simp]
theorem hasDerivWithinAt_diff_singleton : HasDerivWithinAt f f' (s \ { x }) x ↔ HasDerivWithinAt f f' s x :=
  hasFDerivWithinAt_diff_singleton _

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