English
If I is a manifold of class n on M, then the transported model I.transContinuousLinearEquiv e is also a manifold of class n on M; the transport preserves the differentiable structure up to the class n.
Русский
Если I является многообразием класса n на M, то преобразованная модель I.transContinuousLinearEquiv e также является многообразием класса n на M; переход сохраняет дифференцируемую структуру до класса n.
LaTeX
$$$\text{IsManifold}(I, n, M) \implies \text{IsManifold}(I.transContinuousLinearEquiv e, n, M)$$$
Lean4
instance instIsManifoldtransContinuousLinearEquiv [IsManifold I n M] :
IsManifold (I.transContinuousLinearEquiv e) n M :=
by
refine isManifold_of_contDiffOn (I.transContinuousLinearEquiv e) n M fun e₁ e₂ h₁ h₂ => ?_
refine e.contDiff.comp_contDiffOn (((contDiffGroupoid n I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn ?_)
simp [preimage_comp, range_comp, mapsTo_iff_subset_preimage, ContinuousLinearEquiv.image_eq_preimage]
