Mathlib.Geometry.Manifold

For a C² embedding of a finite-dimensional manifold, possibly with boundary or corners, into a Euclidean space, this part of the library defines the tangent space at a point as the range of the differential and the norma

Embedded­Normal­Geometry 25 core · 49 supporting · 3 submodules Let f be a C² embedding of a finite-dimensional manifold M, possibly with boundary or corners, into a finite-dimensional Euclidean space.