English
In the field case, fderivWithin of c · f equals c times fderivWithin f, when considering within s at x.
Русский
В случае поля, fderivWithin (c · f) на s в x равно c · fderivWithin f на s в x.
LaTeX
$$$ fderivWithin 𝕜 (c \cdot f) \, s \, x = c \, fderivWithin 𝕜 f \, s \, x$ для invertible c, включая нулевой случай через соответствующие леммы.$$
Lean4
/-- A version of `fderivWithin_const_smul` without differentiability hypothesis:
in return, the constant `c` must be invertible, i.e. if `R` is a field. -/
theorem fderivWithin_const_smul_of_invertible (c : R) [Invertible c] (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x :=
by
by_cases h : DifferentiableWithinAt 𝕜 f s x
· exact (h.hasFDerivWithinAt.const_smul c).fderivWithin hs
· obtain (rfl | hc) := eq_or_ne c 0
· simp
have : ¬DifferentiableWithinAt 𝕜 (c • f) s x := by
contrapose! h
exact (differentiableWithinAt_smul_iff c).mp h
simp [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this]
