Immersions and smooth embeddings

Stream: PR reviews

[Michael Rothgang]

I think I have found a good way to formalise immersions and smooth embeddings, in a manner encompassing infinite-dimensional manifolds. As my overall PR #23040 is growing large (around 1000 lines already), let me open this topic to track the overall progress.
Proving everything nice one would like about immersions and embeddings is still a moment away (as this requires the inverse function theorem), but quite a few things can already be said.

Already reviewable are

• #23175 (an injective bounded linear operator has closed range iff it is anti-Lipschitz) and
• #23219 (preliminaries about local diffeomorphisms)

The latter will also unblock #8738, which has been sitting idle for about a year now.

[Michael Rothgang]

Thanks for the two reviews already! The next PR in this series is #8738 (local diffeomorphisms have isomorphic differential).