English
If hc is HasStrictDerivAt for c with derivative c' and d is a constant, then (y ↦ c(y) · d) has derivative c' · d at x.
Русский
Если c имеет строгую производную в x и d константа, то производная от y ↦ c(y) · d равна c'(x) · d.
LaTeX
$$$\text{HasStrictDerivAt}(y \mapsto c(y) \cdot d) x = c'(x) \cdot d$$$
Lean4
theorem derivWithin_mul_const_field (u : 𝕜') : derivWithin (fun y => v y * u) s x = derivWithin v s x * u :=
by
by_cases hv : DifferentiableWithinAt 𝕜 v s x
· rw [derivWithin_mul_const hv u]
by_cases hu : u = 0
· simp [hu]
rw [derivWithin_zero_of_not_differentiableWithinAt hv, zero_mul, derivWithin_zero_of_not_differentiableWithinAt]
have : v = fun x ↦ (v x * u) * u⁻¹ := by ext; simp [hu]
exact fun h_diff ↦ hv <| this ▸ h_diff.mul_const _
