iteratedFDerivWithin_const_smul_apply

English

The scalar multiplication by a constant preserves ContDiffOn 𝕜 n: c • f is ContDiffOn 𝕜 n on s if f is ContDiffOn 𝕜 n on s.

Русский

Константное умножение сохраняет ContDiffOn.

LaTeX

$$$\\\\forall c \\\\in R, \\\\forall f \\\\in ContDiffOn 𝕜 n f s, \\\\ ContDiffOn 𝕜 n (\\\\lambda y. c \\\\cdot f y) s$$

Lean4

theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffWithinAt 𝕜 i f s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x :=
  (a • (1 : F →L[𝕜] F)).iteratedFDerivWithin_comp_left hf hu hx le_rfl

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