differentiableWithinAt_const_sub_iff

English

Equivalence between differentiability within s of y ↦ c − f(y) and differentiability within s of f(y).

Русский

Эквивалентность между дифференцируемостью внутри s для y ↦ c − f(y) и для f(y).

LaTeX

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

Lean4

@[simp]
theorem differentiableWithinAt_const_sub_iff (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x := by simp [sub_eq_add_neg]

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