add CHANGELOG entries

math-comp · Jul 30, 2021 · 75ef866 · 75ef866
1 parent f36316e
commit 75ef866
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -19,6 +19,8 @@
   + lemma `bigcup_set_cond`
 - in `classical_sets.v`:
   + lemmas `bigcupD1`, `bigcapD1`
+- in `normedtypes.v`:
+  + lemma `is_intervalPlt`
 
 ### Changed
 
@@ -39,6 +41,7 @@
 - in `normedtype.v`:
   + lemma `cvg_bounded_real`
   + lemma `pseudoMetricNormedZModType_hausdorff`
+  + definition `is_interval`
 
 ### Changed
 
@@ -122,6 +125,9 @@
 - in `nngnum.v`:
   + lemma `filter_andb`
 
+- in `normedtype.v`:
+  + lemma `is_intervalPle`
+
 ### Infrastructure
 
 ### Misc