smul_const — Mathlib

English

If c is differentiable on s, then y ↦ c(y) · f is differentiable on s for any fixed f ∈ F.

Русский

Если c дифференцируема на множестве s, то функция y ↦ c(y) · f дифференцируема на s для любого фиксированного f ∈ F.

LaTeX

$$$\ DifferentiableOn\ 𝕜\ c\ s\ \Rightarrow \ DifferentiableOn\ 𝕜\ (\\lambda y. c(y) \\cdot f)\ s$$$

Lean4

@[fun_prop]
theorem smul_const (hc : DifferentiableOn 𝕜 c s) (f : F) : DifferentiableOn 𝕜 (fun y => c y • f) s := fun x hx =>
  (hc x hx).smul_const f

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