const_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 a constant and a `C^n` on a domain is `C^n`. -/
@[fun_prop]
theorem const_smul {s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun y => c • f y) s :=
  fun x hx => (hf x hx).const_smul c

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