clm_apply — Mathlib

English

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

Русский

Если f: E → StrongDual 𝕜 F и g: E → G гладкие порядка n, то x ↦ (f x).smulRight (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 \mathrm{f}(x) \smulRight \mathrm{g}(x)).$$$

Lean4

@[fun_prop]
theorem clm_apply {f : E → F →L[𝕜] G} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => (f x) (g x)) x :=
  isBoundedBilinearMap_apply.contDiff.comp₂_contDiffAt hf hg

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