clm_postcomp — Mathlib

English

If a family of postcomposition maps is ContMDiffOn on s, then the composed map is ContMDiffOn on s.

Русский

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

LaTeX

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

Lean4

nonrec theorem clm_postcomp {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).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) s :=
  fun x hx ↦ (hf x hx).clm_postcomp

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