format doc (#1130)

* format doc --------- Co-authored-by: Pierre Roux <[email protected]>
math-comp · Jan 9, 2024 · 1fd0e85 · 1fd0e85
1 parent aed4ed5
commit 1fd0e85
Show file tree

Hide file tree

Showing 3 changed files with 309 additions and 238 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -120,6 +120,8 @@
 
 - in `sequences.v`:
   + change the implicit arguments of `trivIset_seqDU`
+- moved from `topology.v` to `mathcomp_extra.v`
+  + definition `monotonous`
 
 ### Renamed
 

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -27,6 +27,8 @@ From mathcomp Require Import finset interval.
 (*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
 (*                           given x : T i                                    *)
 (*                 swap x := (x.2, x.1)                                       *)
+(*         monotonous A f := {in A &, {mono f : x y / x <= y}} \/             *)
+(*                           {in A &, {mono f : x y /~ x <= y}}               *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -929,3 +931,6 @@ exists n.+1; rewrite nm2/= -addn1.
 rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
 by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
 Qed.
+
+Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) :=
+  {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}.