generalizations

math-comp · Jan 11, 2024 · 560dcfc · 560dcfc
1 parent b0d400f
commit 560dcfc
Show file tree

Hide file tree

Showing 2 changed files with 174 additions and 113 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,11 @@
 
 ### 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`
+
 ### Deprecated
 
 ### Removed