smul — Mathlib

English

If c is differentiable on s and f is differentiable on s, then x ↦ c(x) · f(x) is differentiable on s.

Русский

Если c и f дифференцируемы на s, то точечное произведение c(x) · f(x) дифференцируемо на s.

LaTeX

$$$\text{DiffContOnCl}(\mathfrak{c}, s) \land \text{DiffContOnCl}(f, s) \Rightarrow \text{DiffContOnCl}(x \mapsto c(x) \cdot f(x), s).$$$

Lean4

theorem smul {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
    {c : E → 𝕜'} {f : E → F} {s : Set E} (hc : DiffContOnCl 𝕜 c s) (hf : DiffContOnCl 𝕜 f s) :
    DiffContOnCl 𝕜 (fun x => c x • f x) s :=
  ⟨hc.1.smul hf.1, hc.2.smul hf.2⟩

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