changelog

CHANGELOG_UNRELEASED.md

@@ -110,6 +110,26 @@
   + canonical `mul_inum`
   + lemmas `inum_eq`, `inum_le`, `inum_lt`
 
+- in file `cantor.v`,
+  + new definitions `countable_nat`, `totally_disconnected`, `countable_basis`, 
+    `cantor_like`, `pointedDiscrete`, and `tree_of`.
+  + new lemmas `bool2E`, `bool_predE`, `cantor_space_compact`, 
+    `cantor_space_hausdorff`, `perfect_set2`, `totally_disconnected_prod`, 
+    `totally_disconnected_discrete`, `cantor_totally_disconnected`, 
+    `cantor_perfect`, `cantor_like_cantor_space`, `totally_disconnected_cvg`, 
+    `clopen_countable`, `compact_countable_base`, `tree_map_props`, 
+    `homeomorphism_cantor_like`, `cantor_like_finite_prod`, `ent_closure`, and 
+    `cantor_surj`.
+- in file `topology.v`,
+  + new definitions `discrete_ent`, `discrete_ent_filter`, 
+    `discrete_uniform_mixin`, `discrete_uniformType`, `discrete_ball`, 
+    `discrete_pseudoMetricType_mixin`, `discrete_pseudoMetricType`, and 
+    `pseudoMetric_bool`.
+  + new lemmas `finite_compact`, `discrete_ent_refl`, `discrete_ent_inv`, 
+    `discrete_ent_split`, `discrete_ent_nbhs`, `discrete_ball_center`, 
+    `discrete_ball_sym`, `discrete_ball_triangle`, `discrete_entourage`, and 
+    `compact_cauchy_cvg`.
+
 ### Changed
 
 - in `mathcomp_extra.v`