# Smooth Manifolds

 Title: Smooth Manifolds Authors: Fabian Immler and Bohua Zhan Submission date: 2018-10-22 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. BibTeX: @article{Smooth_Manifolds-AFP, author = {Fabian Immler and Bohua Zhan}, title = {Smooth Manifolds}, journal = {Archive of Formal Proofs}, month = oct, year = 2018, note = {\url{https://isa-afp.org/entries/Smooth_Manifolds.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License