smul — Mathlib

English

For a nonzero scalar c, UniqueDiffWithinAt 𝕜 s x is equivalent to UniqueDiffWithinAt 𝕜 (c • s) (c • x).

Русский

При ненулевом скаляре c, UniqueDiffWithinAt 𝕜 s x эквивалентно UniqueDiffWithinAt 𝕜 (c • s) (c • x).

LaTeX

$$$$ \\text{UniqueDiffWithinAt } 𝕜 (\\mathrm{instHSMul.hSMul } c\, s) (\\mathrm{instHSMul.hSMul } c\, x) \\iff \\text{UniqueDiffWithinAt } 𝕜 s x $$$$

Lean4

protected theorem smul (h : UniqueDiffWithinAt 𝕜 s x) {c : 𝕜} (hc : c ≠ 0) : UniqueDiffWithinAt 𝕜 (c • s) (c • x) :=
  (ContinuousLinearEquiv.smulLeft <| Units.mk0 c hc).hasFDerivWithinAt |>.uniqueDiffWithinAt_of_continuousLinearEquiv _
    h

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