fun_const_smul — Mathlib

English

If ω is ContDiffOn r ω s and hr, hs hold, then theExtDerivWithin of ω is zero on s ∩ closure(interior s).

Русский

Если ω достаточно гладкая на s, и выполняются условия hr, hs, то extDerivWithin( extDerivWithin ω s) равно нулю на s ∩ closure(interior s).

LaTeX

$$$ h_ω : ContDiffOn 𝕜 r ω s \\rightarrow hr : minSmoothness 𝕜 2 ≤ r \\rightarrow hs : UniqueDiffOn 𝕜 s \\rightarrow EqOn (extDerivWithin (extDerivWithin ω s) s) 0 (s ∩ closure (interior s)) $$$

Lean4

@[fun_prop]
nonrec theorem fun_const_smul (h : HasFDerivWithinAt f f' s x) (c : R) :
    HasFDerivWithinAt (fun x => c • f x) (c • f') s x :=
  h.const_smul c

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