Metamath Proof Explorer


Table of Contents - 20.3.14.7. Topological Manifolds

Found this and was curious about how manifolds would be expressed in set.mm: https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover

This chapter proposes to define first manifold topologies, which characterize topological manifolds, and then to extend the structure with presentations, i.e., equivalence classes of atlases for a given topological space. We suggest to use the extensible structures to define the "topological space" aspect of topological manifolds, and then extend it with charts/presentations.

  1. cmntop
  2. df-mntop
  3. relmntop
  4. ismntoplly
  5. ismntop