Mathlib.Geometry

Geometry infrastructure extending Mathlib: tangent and normal spaces, normal bundles, and shape operators of smooth embedded submanifolds of Euclidean space.

Manifold 25 core · 49 supporting · 1 submodule 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