cle_arrowCongr — Mathlib

English

Global differentiability of arrowCongr: if f and g are differentiable, then the map x ↦ (f x).arrowCongr (g x) is differentiable.

Русский

Глобальная дифференцируемость arrowCongr: отображение x ↦ (f x).arrowCongr (g x).

LaTeX

$$$$MDifferentiable I 𝓘(𝕜, (F_1 \to_L F_3) \to_L (F_2 \to_L F_4)) (\lambda x. (f x).arrowCongr (g x))$$$$

Lean4

theorem cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
    (hf : MDifferentiable I 𝓘(𝕜, F₂ →L[𝕜] F₁) (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)))
    (hg : MDifferentiable I 𝓘(𝕜, F₃ →L[𝕜] F₄) (fun x ↦ (g x : F₃ →L[𝕜] F₄))) :
    MDifferentiable I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄))
      (fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) :=
  fun x ↦ (hf x).cle_arrowCongr (hg x)

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