clm_apply — Mathlib

English

If g and f are ContMDiffOn on s, then the pointwise application is ContMDiffOn on s.

Русский

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

LaTeX

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

Lean4

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

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