const_smul — Mathlib

English

If f is differentiable on s with continuous derivative, then c • f is differentiable on s for any scalar c from a semiring R with appropriate structure.

Русский

Если f дифференцируема на s, то константное умножение c · f дифференцируемо на s для любого скаляра c из поля/кольца, обладающего нужной структурой.

LaTeX

$$$\forall R\text{ with } \dots,\; \text{DiffContOnCl}(\mathit{f}, s) \Rightarrow \text{DiffContOnCl}(c \cdot \mathit{f}, s).$$$

Lean4

theorem const_smul {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F]
    (hf : DiffContOnCl 𝕜 f s) (c : R) : DiffContOnCl 𝕜 (c • f) s :=
  ⟨hf.1.const_smul c, hf.2.const_smul c⟩

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