adding changelog

math-comp · Nov 10, 2024 · 4c5f01b · 4c5f01b
1 parent 08592f2
commit 4c5f01b
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -77,6 +77,10 @@
   + new lemmas `swap_continuous`, `prodA_continuous`, and 
     `prodAr_continuous`.
 
+- in file `order_topology.v`
+  + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
+    `max_fun_continuous`.
+
 ### Changed
 
 - in file `normedtype.v`,