Manuel Eberl
2018-10-23 14:41:34 UTC
I am happy to be able to announce a new AFP entry on a subject that I am
personally very interested in:
Smooth Manifolds
by Fabian Immler and Bohua Zhan
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.
https://www.isa-afp.org/entries/Smooth_Manifolds.html
Enjoy!
Manuel
personally very interested in:
Smooth Manifolds
by Fabian Immler and Bohua Zhan
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.
https://www.isa-afp.org/entries/Smooth_Manifolds.html
Enjoy!
Manuel