clm_comp — Mathlib

English

If g: M → F1 →L F2 and f: M → F1 are ContMDiffOn on s, then the map x ↦ g(x)(f(x)) is ContMDiffOn on s.

Русский

Если g и f гладкие на s, то точечное применение гладкое на s.

LaTeX

$$$\\forall s, x,\\ ContMDiffOn I 𝓘(𝕜, F_1 \\to_L F_2) n g s \\land ContMDiffOn I 𝓘(𝕜, F_1) n f s \\Rightarrow ContMDiffOn I 𝓘(𝕜, F_2) n (fun x => g x (f x)) s.$$$

Lean4

theorem clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s)
    (hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s :=
  fun x hx => (hg x hx).clm_comp (hf x hx)

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