hasFDerivAt_sub_const — Mathlib

English

Differentiability within a set of the function y ↦ f(y) − c at x is equivalent to differentiability of f at x within the same set.

Русский

Дифференцируемость внутри множества функции y ↦ f(y) − c в точке x эквивалентна дифференцируемости функции f в x внутри того же множества.

LaTeX

$$$ DifferentiableWithinAt 𝕜 (\\lambda y, f(y) - c) \\\\ s \\\\ x \\iff DifferentiableWithinAt 𝕜 f s x $$$

Lean4

@[fun_prop]
theorem hasFDerivAt_sub_const {x : F} (c : F) : HasFDerivAt (· - c) (.id 𝕜 F) x :=
  (hasFDerivAt_id x).sub_const c

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