differentiableWithinAt_const_add_iff

English

For any fixed c ∈ F and any subset s, the function y ↦ c + f(y) is differentiable within s at x if and only if f is differentiable within s at x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem differentiableWithinAt_const_add_iff (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => c + f y) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  exists_congr fun _ ↦ hasFDerivWithinAt_const_add_iff c

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