hasFDerivWithinAt_diff_singleton — Mathlib

English

If HasFDerivWithinAt f f' {x} y holds, then DifferentiableWithinAt 𝕜 f {x} y holds.

Русский

Если HasFDerivWithinAt f f' {x} y выполняется, тогда DifferentiableWithinAt 𝕜 f {x} y выполняется.

LaTeX

$$$$\\text{HasFDerivWithinAt } f\\,f'\\{ x \\} \\{ y \\} \\implies \\text{DifferentiableWithinAt } 𝕜 f \\{ x \\} \\{ y \\}.$$$$

Lean4

@[simp]
theorem hasFDerivWithinAt_diff_singleton (y : E) : HasFDerivWithinAt f f' (s \ { y }) x ↔ HasFDerivWithinAt f f' s x :=
  by rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]

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