clm_precomp — Mathlib

English

Global differentiability of the precomposition map: the map y ↦ (f y).precomp F3 is differentiable if f is differentiable.

Русский

Глобальная дифференцируемость предкомпоновки: отображение y ↦ (f y).precomp F3 дифференцируемо, если f дифференцируемо.

LaTeX

$$$$ \forall f: M \to F_1 \to_L[\mathbb{K}] F_2, \ MDifferentiable I 𝓘(𝕜, F_1 \to_L[𝕜] F_2) f \Rightarrow MDifferentiable I 𝓘(𝕜, (F_2 \to_L[𝕜] F_3) \to_L[𝕜] (F_1 \to_L[𝕜] F_3)) (\lambda y. (f(y)).precomp F_3). $$$$

Lean4

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

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