Smooth Manifolds

Fabian Immler 🌐 and Bohua Zhan 🌐

October 22, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem of path integrals. We also examine some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the analysis and linear algebra libraries in Isabelle/HOL, in particular its “types-to-sets” mechanism.


BSD License


Session Smooth_Manifolds