smul_const — Mathlib

English

If c is differentiable on s and y is fixed in F, then x ↦ c(x) · y is differentiable on s.

Русский

Если c непрерывно дифференцируема на s и фиксированная величина y ∈ F, то x ↦ c(x) · y дифференцируема на s.

LaTeX

$$$\text{DiffContOnCl}(\mathord{\mathbb{c}}, s) \Rightarrow \text{DiffContOnCl}(x \mapsto c(x) \cdot y, s).$$$

Lean4

theorem smul_const {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F]
    [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {s : Set E} (hc : DiffContOnCl 𝕜 c s) (y : F) :
    DiffContOnCl 𝕜 (fun x => c x • y) s :=
  hc.smul diffContOnCl_const

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