| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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 |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |