Give specific examples

[stop-cran]

Maybe it'd be useful to give some simple and practical examples to the defined topological constructions and proven theorems. E. g. a homeomorphism between a unit interval with identified ends and a unit circle.

[Columbus240]

A nice way to define spheres, would be as SubspaceTopology (inverse_image (euclidean_norm_on_R^n) (Singleton 1)). So some theory about finite products and finite dimensional euclidean spaces would be useful in this setting.
Using the Heine-Borel property of R^n we can then show that spheres are compact.

I made a sketch on a separate branch.

While playing around, I noticed that working with SubspaceTopology is very clunky and needs a lot of boilerplate, translating between X and { x : X | In S x }. Doing this to functions & ensembles makes everything a lot more difficult.
How about introducing a notion of "open_in_subspace" or somesuch, as

Definition open_in_subspace
  {X : TopologicalSpace}
  (S : Ensemble (point_set X))
  (U : Ensemble (point_set X)) :=
    Included U S /\ exists U', open U' /\ U = Intersection S U'.

And similar notion for compactness? Or at least a lemma that maps from U : Ensemble (point_set (SubspaceTopology S)), open U to open_in_subspace.

[Columbus240]

The definition open_in_subspace is unnecessary, now that subspace_open_char is an equivalence. But more a definition of compact_subspace would still be nice.

Some more example spaces & constructions:

• discrete & indiscrete spaces
• Sierpinski space (leading to some characterization theorems of other properties)
• cofinite & cocountable topologies
• theory of euclidean spaces and their subsets

[Columbus240]

Some possible constructions and isomorphisms:

• ℝ^n / ℤ^n is homeomorphic to the n-fold product of S^1, which is called "the n-dimensional torus". The quotient map from ℝ^n to the torus is the universal cover.
• The n-spheres S^n are one-point-compactifications of ℝ^n.