Email Gateway (Aug 22 2022 at 18:40): Email Gateway (Aug 22 2022 at 18:40):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC