clm_comp — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{If } hg : ContMDiffWithinAt I 𝓘(𝕜, F_1 \\to_L F_2) n g s x\\ and\\ hf : ContMDiffWithinAt I 𝓘(𝕜, F_1) n f s x,\\ then\\ ContMDiffWithinAt I 𝓘(𝕜, F_2) n (fun x => g x (f x)) s x.$$$

Lean4

theorem clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x)
    (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) x :=
  (hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem

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