From 7d32a04825f148c80424f47f418ebbcb8981a216 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 16 Nov 2023 16:38:07 +0900 Subject: [PATCH] doc --- theories/realfun.v | 5 +++++ theories/sequences.v | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/theories/realfun.v b/theories/realfun.v index 5d32e814ff..64f4cf6c3f 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -11,6 +11,11 @@ From HB Require Import structures. (* This file provides properties of standard real-valued functions over real *) (* numbers (e.g., the continuity of the inverse of a continuous function). *) (* *) +(* nondecreasing_fun f == the function f is non-decreasing *) +(* nonincreasing_fun f == the function f is non-increasing *) +(* increasing_fun f == the function f is (strictly) increasing *) +(* decreasing_fun f == the function f is (strictly) increasing *) +(* *) (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) (* *) diff --git a/theories/sequences.v b/theories/sequences.v index 1715058381..70caecc5c3 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -11,6 +11,11 @@ Require Import reals ereal signed topology normedtype landau. (* The purpose of this file is to gather generic definitions and lemmas about *) (* sequences. *) (* *) +(* nondecreasing_seq u == the sequence u is non-decreasing *) +(* nonincreasing_seq u == the sequence u is non-increasing *) +(* increasing_seq u == the sequence u is (strictly) increasing *) +(* decreasing_seq u == the sequence u is (strictly) increasing *) +(* *) (* * About sequences of real numbers: *) (* [sequence u_n]_n == the sequence of general element u_n *) (* R ^nat == notation for the type of sequences, i.e., *)