clm_comp — Mathlib

English

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

Русский

Если g и f гладкие композиционно, то композиция g(x) ∘ f(x) гладкая.

LaTeX

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

Lean4

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

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