clm_precomp — Mathlib

English

If f: M → F2 →L F3 is ContMDiffOn on s, then the postcomposition map x ↦ f(x).postcomp F1 is ContMDiffOn on s.

Русский

Если f гладко на множестве s, то отображение x ↦ f(x).postcomp F1 гладко на s.

LaTeX

$$$\\text{If } f: M \\to F_2 \\to_L F_3\\text{ is ContMDiffOn } I\\, 𝓘(𝕜, F_2 \\to_L F_3)\\, n f s,\\ \\text{then } x \\mapsto (f(x)).postcomp F_1\\text{ is ContMDiffOn } I\\, 𝓘(𝕜, (F_1 \\to_L F_2) \\to_L F_3)\\, n$ on s.$$

Lean4

theorem clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} (hf : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s) :
    ContMDiffOn I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) n
      (fun y ↦ (f y).precomp F₃ : M → (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) s :=
  fun x hx ↦ (hf x hx).clm_precomp

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