### 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

BSD License

### Topics

- Mathematics/Analysis
- Mathematics/Topology

### 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

## Cite

×

Smooth_Manifolds-AFP

    @article{Smooth_Manifolds-AFP,
      author  = {Fabian Immler and Bohua Zhan},
      title   = {Smooth Manifolds},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Smooth_Manifolds.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Oct 23, 2018 : Isabelle2018