smul — Mathlib

English

If h : LineDifferentiableWithinAt 𝕜 f s x v, then for any scalar c, f is line differentiable within s at x for direction c v.

Русский

Если h : LineDifferentiableWithinAt 𝕜 f s x v, то при любом скаляре c функция f дифференцируема вдоль направления c v внутри s.

LaTeX

$$$$ HasLineDerivWithinAt 𝕜 f s x v \Rightarrow LineDifferentiableWithinAt 𝕜 f s x (c \cdot v) $$$$

Lean4

theorem smul (h : LineDifferentiableWithinAt 𝕜 f s x v) (c : 𝕜) : LineDifferentiableWithinAt 𝕜 f s x (c • v) :=
  (h.hasLineDerivWithinAt.smul c).lineDifferentiableWithinAt

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