contDiff_smul — Mathlib

English

If f: E → 𝕜 and g: E → F are ContDiff 𝕜 n at x, then the product y ↦ f(y)·g(y) is ContDiff 𝕜 n at x.

Русский

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

LaTeX

$$$\\\\forall f : E \\to 𝕜, g : E \\to F, \\\\ ContDiff 𝕜 n f x \\\\Rightarrow \\\\ ContDiff 𝕜 n g x \\\\Rightarrow \\\\ ContDiff 𝕜 n (\\\\lambda y. f(y) \\\\cdot g(y)) x$$

Lean4

@[fun_prop]
theorem contDiff_smul : ContDiff 𝕜 n fun p : 𝕜 × F => p.1 • p.2 :=
  isBoundedBilinearMap_smul.contDiff

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