extDerivWithin_fun_smul — Mathlib

English

For a scalar c in 𝕜 and ω a differential form, extContOnCl and scalar multiplication commute: extDeriv (c • ω) = c • extDeriv ω.

Русский

Умножение дифференцируемого форм на скаляр c сохраняет дифференцируемость: extDeriv (c • ω) = c • extDeriv ω.

LaTeX

$$$\text{extDeriv}(c \cdot \omega) = c \cdot \text{extDeriv}(\omega).$$$

Lean4

theorem extDerivWithin_fun_smul (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) (hsx : UniqueDiffWithinAt 𝕜 s x) :
    extDerivWithin (fun x ↦ c • ω x) s x = c • extDerivWithin ω s x :=
  extDerivWithin_smul c ω hsx

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