English
If f and g are differentiable withinAt, then the arrowCongr map sending y to (f y).arrowCongr (g y) is differentiable on s.
Русский
Если f и g дифференцируемы, то отображение y ↦ (f y).arrowCongr (g y) дифференцируемо на s.
LaTeX
$$$$MDifferentiableWithinAt I 𝓘(𝕜, (F_1 \to_L F_3) \to_L (F_2 \to_L F_4)) (\lambda y. (f y).arrowCongr (g y)) s x$$$$
Lean4
theorem cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M}
(hf : MDifferentiableOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s)
(hg : MDifferentiableOn I 𝓘(𝕜, F₃ →L[𝕜] F₄) (fun x ↦ (g x : F₃ →L[𝕜] F₄)) s) :
MDifferentiableOn I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄))
(fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) s :=
fun x hx ↦ (hf x hx).cle_arrowCongr (hg x hx)
