format doc (#1130)

* format doc --------- Co-authored-by: Pierre Roux <[email protected]>
math-comp · Jan 7, 2024 · 437d12c · 437d12c
1 parent 74b4d4f
commit 437d12c
Show file tree

Hide file tree

Showing 3 changed files with 310 additions and 239 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -115,6 +115,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
@@ -30,6 +30,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}}               *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -1485,3 +1487,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}}.