generalizations (#1147)

* generalizations
math-comp · Jan 18, 2024 · cb07aa9 · cb07aa9
1 parent 1c0b3be
commit cb07aa9
Show file tree

Hide file tree

Showing 2 changed files with 227 additions and 126 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -22,6 +22,14 @@
 
 ### Generalized
 
+- in `realfun.v`:
+  + lemmas `nonincreasing_at_right_cvgr`, `nonincreasing_at_left_cvgr`
+  + lemmas `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
+    `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
+
+- in `realfun.v`:
+  + lemmas `nonincreasing_at_right_is_cvgr`, `nondecreasing_at_right_is_cvgr`
+
 ### Deprecated
 
 ### Removed