feat: smooth immersions (leanprover-community#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

Co-authored-by: Christian Merten <christian@merten.dev>

Author: grunweg

Mathlib.lean

@@ -4154,6 +4154,7 @@ public import Mathlib.Geometry.Manifold.ContMDiffMap
 public import Mathlib.Geometry.Manifold.DerivationBundle
 public import Mathlib.Geometry.Manifold.Diffeomorph
 public import Mathlib.Geometry.Manifold.GroupLieAlgebra
+public import Mathlib.Geometry.Manifold.Immersion
 public import Mathlib.Geometry.Manifold.Instances.Icc
 public import Mathlib.Geometry.Manifold.Instances.Real
 public import Mathlib.Geometry.Manifold.Instances.Sphere
@@ -4167,6 +4168,7 @@ public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
 public import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
 public import Mathlib.Geometry.Manifold.LocalDiffeomorph
 public import Mathlib.Geometry.Manifold.LocalInvariantProperties
+public import Mathlib.Geometry.Manifold.LocalSourceTargetProperty
 public import Mathlib.Geometry.Manifold.MFDeriv.Atlas
 public import Mathlib.Geometry.Manifold.MFDeriv.Basic
 public import Mathlib.Geometry.Manifold.MFDeriv.Defs