Alexandroff-Hausdorff Theorem and the Cantor Space

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,18 @@
 
 ### Added
 
+- in file `cantor.v`,
+  + new definitions `cantor_space`, `cantor_like`, `pointed_discrete`, and 
+    `tree_of`.
+  + new lemmas `cantor_space_compact`, `cantor_space_hausdorff`, 
+    `cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`, 
+    `tree_map_props`, `homeomorphism_cantor_like`, and 
+    `cantor_like_finite_prod`.
+  + new theorem `cantor_surj`.
+- in file `topology.v`,
+  + new lemmas `perfect_set2`, and `ent_closure`.
+  + lemma `clopen_surj`
+
 ### Changed
 
 ### Renamed

_CoqProject

@@ -22,6 +22,7 @@ theories/reals.v
 theories/landau.v
 theories/Rstruct.v
 theories/topology.v
+theories/cantor.v
 theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v