smul — Mathlib

English

If h : HasLineDerivAt 𝕜 f f' x v, then for any scalar c, HasLineDerivAt 𝕜 f (c • f') x (c • v).

Русский

Если h : HasLineDerivAt 𝕜 f f' x v, то для любого скаляра c имеет место HasLineDerivAt 𝕜 f (c • f') x (c • v).

LaTeX

$$$$ HasLineDerivAt 𝕜 f f' x v \Rightarrow HasLineDerivAt 𝕜 f (c \cdot f') x (c \cdot v) $$$$

Lean4

theorem smul (h : HasLineDerivAt 𝕜 f f' x v) (c : 𝕜) : HasLineDerivAt 𝕜 f (c • f') x (c • v) :=
  by
  simp only [← hasLineDerivWithinAt_univ] at h ⊢
  exact HasLineDerivWithinAt.smul h c

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