Commit 2025-11-28 19:37 fc14f3da

feat: smooth immersions (#28793) Define smooth immersions between manifolds. We use a definition which allows for corners, infinite dimension and arbitrary fields. This matches the mathematical literature for e.g. real Banach manifolds with corners (even though there is no textbook treating manifolds as general as mathlib's). This PR provides four central definitions: being an immersion at a point, and being an immersion everywhere, plus a variant of these with a fixed complement. (Being an immersion at a point is a property with respect to some choice of complement in the model normed space of the codomain. In most applications, there is no need to control this complement. Such control will be helpful, however, when considering the local characterisation of submanifolds: locally, a submanifold is described either as the image of an immersion, or the preimage of a submersion