clm_postcomp — Mathlib

English

If hf: ContMDiffAt I 𝓘(𝕜, F2 →L F3) n f at x, then ContMDiffAt I 𝓘(𝕜, (F1 →L F2) →L F1 →L F3) n (fun y => (f y).postcomp F1) at x.

Русский

Если hf гладко в точке, то отображение посткомпозиций гладко в точке.

LaTeX

$$$\\text{If } hf : ContMDiffAt I 𝓘(𝕜, F_2 \\to_L F_3) n f x,\\ \\text{then } ContMDiffAt I 𝓘(𝕜, (F_1 \\to_L F_2) \\to_L (F_1 \\to_L F_3)) n (fun y => (f y).postcomp F_1) x.$$$

Lean4

nonrec theorem clm_postcomp {f : M → F₂ →L[𝕜] F₃} {x : M} (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f x) :
    ContMDiffAt I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) n
      (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) x :=
  hf.clm_postcomp

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