clm_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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