smul — Mathlib

English

Same as above, restated in a form suitable for differentiation on s.

Русский

То же самое, переформулированное для дифференцирования внутри s.

LaTeX

$$$$ \\DifferentiableWithinAt 𝕜 c s x \\rightarrow \\DifferentiableWithinAt 𝕜 f s x \\rightarrow \\DifferentiableWithinAt 𝕜 (fun y => c y · f y) s x $$$$

Lean4

@[fun_prop]
theorem smul (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 (c • f) s x :=
  (hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).differentiableWithinAt

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