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

-- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
affeldt-aist · Nov 16, 2023 · f7a928b · f7a928b
1 parent bd1e2ac
commit f7a928b
Show file tree

Hide file tree

Showing 4 changed files with 623 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,23 @@
 
 ### 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`
+
+- in `cantor.v`:
+  + definition `pointed_discrete0`
+  + lemmas `discrete_space_pointed`, `discrete_pointed`
+  + lemma `bool_compact'`
+
 ### 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