Alexandroff-Hausdorff Theorem and the Cantor Space (#834)

-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Nov 14, 2023 · c518e2a · c518e2a
1 parent 1d41dfe
commit c518e2a
Show file tree

Hide file tree

Showing 4 changed files with 582 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/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

diff --git a/_CoqProject b/_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