clm_apply — Mathlib

English

If g: M → F1 →L F2 and f: M → F1 are ContMDiffAt, then x ↦ g x (f x) is ContMDiffAt.

Русский

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

LaTeX

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

Lean4

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

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