English
Let c ∈ F and f : E → F be a differentiable map at x with derivative f'. Then the map y ↦ c + f(y) has the same derivative f' at x; conversely, if c + f has derivative f' at x then f has derivative f' at x.
Русский
Пусть c ∈ F и f : E → F. Тогда производная функции y ↦ c + f(y) в точке x равна той же производной f в точке x; наоборот, если у функции y ↦ c + f(y) существует производная в x с той же производной f', то производная f в x существует и равна f'.
LaTeX
$$$\operatorname{HasFDerivAt}\left(\lambda y. c + f(y)\right)\ f'\ x \quad\iff\quad \operatorname{HasFDerivAt}(f)\ f'\ x$$$
Lean4
@[simp]
theorem hasFDerivAt_const_add_iff (c : F) : HasFDerivAt (c + f ·) f' x ↔ HasFDerivAt f f' x :=
hasFDerivAtFilter_const_add_iff c
