English
If hf and hg are ContMDiffAt for inverses and arrowCongr, then the map x ↦ (f(x).arrowCongr (g(x))) is ContMDiffAt.
Русский
Если hf и hg гладкие для преобразования стрелок и конгруирования, то карта стрелок гладкая.
LaTeX
$$$\\forall x,\\ (hf x).cle_arrowCongr (hg x) \\Rightarrow \\mathrm{ContMDiffAt} I 𝓘(𝕜, (F_1 \\to_L F_3) \\to_L (F_2 \\to_L F_4)) n (fun y => (f y).arrowCongr (g y)) x.$$$
Lean4
theorem cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
(hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)))
(hg : ContMDiff I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x ↦ (g x : F₃ →L[𝕜] F₄))) :
ContMDiff I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
(fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) :=
fun x ↦ (hf x).cle_arrowCongr (hg x)
