clm_postcomp — Mathlib

English

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

Русский

Если f гладко на s, то постпоставляющее отображение гладко на s.

LaTeX

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

Lean4

theorem clm_postcomp {f : M → F₂ →L[𝕜] F₃} {s : Set M} {x : M} (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f s x) :
    ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) n
      (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) s x :=
  ContDiff.comp_contMDiffWithinAt (F' := (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) (g := ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃)
    (ContinuousLinearMap.contDiff _) hf

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