smul — Mathlib

English

If f and g are ContDiffOn 𝕜 n on s, then the product y ↦ f(y)·g(y) is ContDiffOn 𝕜 n on s.

Русский

Если f и g гладкие на s, то их произведение гладко на s.

LaTeX

$$$\\\\forall s \\\\subset E, \\\\ ContDiffOn 𝕜 n f s \\\\Rightarrow \\\\ ContDiffOn 𝕜 n g s \\\\Rightarrow \\\\ ContDiffOn 𝕜 n (\\\\lambda y. f(y) \\\\cdot g(y)) s$$

Lean4

/-- The scalar multiplication of two `C^n` functions on a domain is `C^n`. -/
@[fun_prop]
theorem smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
    ContDiffOn 𝕜 n (fun x => f x • g x) s := fun x hx => (hf x hx).smul (hg x hx)

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