English
If c is invertible, then differentiability within s is preserved under scalar multiplication by c, i.e., DifferentiableWithinAt 𝕜 (c · f) s x ⇔ DifferentiableWithinAt 𝕜 f s x.
Русский
Если c обратим, тогда дифференцируемость внутри s сохраняется при умножении на c: DifferentiableWithinAt 𝕜 (c · f) s x ⇔ DifferentiableWithinAt 𝕜 f s x.
LaTeX
$$$ \text{differentiableWithinAt}_{𝕜}(c \cdot f) \ s\ x \iff \text{differentiableWithinAt}_{𝕜} f \, s \, x$ при [Invertible c].$$
Lean4
/-- If `c` is invertible, `c • f` is differentiable at `x` within `s` if and only if `f` is. -/
theorem differentiableWithinAt_smul_iff (c : R) [Invertible c] :
DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩
apply (h.const_smul ⅟c).congr_of_eventuallyEq ?_ (by simp)
filter_upwards with x using by simp
