From 76051f241eb65c3b25c3512a7c9d00bd976c4773 Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 21 Mar 2023 10:53:07 -0400 Subject: [PATCH] changelog --- CHANGELOG_UNRELEASED.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5b356bc0ab..74a19b905c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`