Metamath Proof Explorer

Table of Contents - Topological Manifolds

Found this and was curious about how manifolds would be expressed in

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