clm_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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