smul — Mathlib

English

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

Русский

Если LineDifferentiableAt 𝕜 f x v, то для любого скаляра c выполняется LineDifferentiableAt 𝕜 f x (c • v).

LaTeX

$$$$ LineDifferentiableAt 𝕜 f x v \Rightarrow LineDifferentiableAt 𝕜 f x (c \cdot v) $$$$

Lean4

theorem smul (h : LineDifferentiableAt 𝕜 f x v) (c : 𝕜) : LineDifferentiableAt 𝕜 f x (c • v) :=
  (h.hasLineDerivAt.smul c).lineDifferentiableAt

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