fun_const_smul — Mathlib

English

If f is differentiable, then the function y ↦ c · f(y) is differentiable.

Русский

Если f дифференцируема, то функция y ↦ c · f(y) дифференцируема.

LaTeX

$$$ \mathrm{Differentiable}_{\mathbb{K}} f \Rightarrow \forall c\in R, \mathrm{Differentiable}_{\mathbb{K}} (c \cdot f) $$$

Lean4

@[fun_prop]
theorem fun_const_smul (h : Differentiable 𝕜 f) (c : R) : Differentiable 𝕜 fun y => c • f y := fun x =>
  (h x).const_smul c

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