Abstract
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.
License
Topics
Session Smooth_Manifolds
- Analysis_More
- Smooth
- Bump_Function
- Chart
- Topological_Manifold
- Differentiable_Manifold
- Partition_Of_Unity
- Tangent_Space
- Cotangent_Space
- Product_Manifold
- Sphere
- Projective_Space