diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 14 |
2 files changed, 14 insertions, 4 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index c28aec2..36498b3 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1786,8 +1786,8 @@ Lemma min_real : {in real &, forall x y, min x y \is real}. Proof. by move=> x y ? ?; case: real_leP. Qed. Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R): - x0 \is real -> {in P, forall t : I, f t \is real} -> - \big[max/x0]_(t <- r | P t) f t \is real. + x0 \is real -> {in P, forall i : I, f i \is real} -> + \big[max/x0]_(i <- r | P i) f i \is real. Proof. by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index b9ed011..c90bc53 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -1146,7 +1146,7 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : order_scope. Notation "> y" := (lt y) : order_scope. Notation "> y :> T" := (> (y : T)) (only parsing) : order_scope. -Notation ">=< y" := (comparable y) : order_scope. +Notation ">=< y" := ([pred x | comparable x y]) : order_scope. Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope. Notation "x <= y" := (le x y) : order_scope. @@ -1172,7 +1172,7 @@ Notation "x < y ?<= 'if' C" := (lteif x y C) : order_scope. Notation "x < y ?<= 'if' C :> T" := ((x : T) < (y : T) ?<= if C) (only parsing) : order_scope. -Notation ">=< x" := (comparable x) : order_scope. +Notation ">=< x" := ([pred y | comparable y x]) : order_scope. Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope. Notation "x >=< y" := (comparable x y) : order_scope. @@ -3231,6 +3231,16 @@ Lemma nmono_leif (f : T -> T) C : forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C). Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed. +Section comparable_big. +Variables op : T -> T -> T. +Hypothesis op_comparable : forall z, {in >=< z &, forall x y, op x y >=< z}. + +Lemma comparable_big x x0 I (P : pred I) F (s : seq I) : + x0 >=< x -> {in P, forall t, F t >=< x} -> + \big[op/x0]_(i <- s | P i) F i >=< x. +Proof. by move=> ? ?; elim/big_ind : _ => // y z; exact: op_comparable. Qed. +End comparable_big. + End POrderTheory. Section ContraTheory. |