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

-- Co-authored-by: zstone1 <[email protected]>
math-comp · Nov 17, 2023 · e3a557e · e3a557e
1 parent bd1e2ac
commit e3a557e
Show file tree

Hide file tree

Showing 4 changed files with 639 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,24 @@
 
 ### 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`:
+  + definitions `pointed_principal_filter`,
+    `pointed_discrete_topology`
+  + lemma `discrete_pointed`
+  + lemma `discrete_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