diff options
| author | Reynald Affeldt | 2020-05-31 00:24:10 +0900 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-06 01:44:09 +0200 |
| commit | 7f355343ee30f72d8ab3ce87f897dc0092e43c29 (patch) | |
| tree | 3654fd4e19da8f63eecbf9a344054035a84af2eb /mathcomp | |
| parent | efed1800a4f2eaa942704ab8bebc60d9a3ac8dfd (diff) | |
tentative changelog
- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 6dbfaf7..f7b2e0f 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -5619,6 +5619,7 @@ Ltac mexact x := by mapply x. Local Notation min := minr. Local Notation max := maxr. +Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index d8bcff1..59de10c 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -74,6 +74,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* For x, y of type T, where T is canonically a porderType d: *) (* x <= y <-> x is less than or equal to y. *) (* x < y <-> x is less than y (:= (y != x) && (x <= y)). *) +(* min x y <-> if x < y then x else y *) +(* max x y <-> if x < y then y else x *) (* x >= y <-> x is greater than or equal to y (:= y <= x). *) (* x > y <-> x is greater than y (:= y < x). *) (* x <= y ?= iff C <-> x is less than y, or equal iff C is true. *) |