differentiableAt_const_add_iff — Mathlib

English

For any c ∈ F, differentiability at x of the map y ↦ c + f(y) is equivalent to differentiability at x of f.

Русский

Для любого c ∈ F дифференцируемость в точке x функции y ↦ c + f(y) эквивалентна дифференцируемости функции f в точке x.

LaTeX

$$$\operatorname{DifferentiableAt}_{\mathbb{k}}\left(\lambda y. c + f(y)\right)\ x \iff \operatorname{DifferentiableAt}_{\mathbb{k}}\left(f\right)\ x$$$

Lean4

@[simp]
theorem differentiableAt_const_add_iff (c : F) : DifferentiableAt 𝕜 (fun y => c + f y) x ↔ DifferentiableAt 𝕜 f x :=
  exists_congr fun _ ↦ hasFDerivAt_const_add_iff c

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