smulRight — Mathlib

English

If f: E → F →L[𝕜] G and g: E → F are ContDiff 𝕜 n, then x ↦ (f x)(g x) is ContDiff 𝕜 n.

Русский

Если f: E → F →L[𝕜] G и g: E → F гладкие порядка n, то x ↦ (f x)(g x) гладко порядка n.

LaTeX

$$$\mathrm{ContDiff}_{\mathbb{k}}\ n\ f \Rightarrow \mathrm{ContDiff}_{\mathbb{k}}\ n\ g \Rightarrow \mathrm{ContDiff}_{\mathbb{k}}\ n\ (x \mapsto (f x)(g x)).$$$

Lean4

@[fun_prop]
theorem smulRight {f : E → StrongDual 𝕜 F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => (f x).smulRight (g x) :=
  isBoundedBilinearMap_smulRight.contDiff.comp₂ (g := fun p => p.1.smulRight p.2) hf hg

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