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