From b0a01acd904cbfcaf47d821b3b5e72098b9efb07 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 3 Sep 2019 17:07:44 +0200 Subject: Add (meet|join)_(l|r), some renamings, and small cleanups New lemmas: - meet_l, meet_r, join_l, join_r. Renamings: - Order.BLatticeTheory.lexUl -> disjoint_lexUl, - Order.BLatticeTheory.lexUr -> disjoint_lexUr, - Order.TBLatticeTheory.lexIl -> cover_leIxl, - Order.TBLatticeTheory.lexIr -> cover_leIxr. Use `Order.TTheory` instead of `Order.Theory` if applicable --- mathcomp/algebra/ssrnum.v | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'mathcomp/algebra/ssrnum.v') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index d068135..2906412 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -125,7 +125,7 @@ Unset Printing Implicit Defensive. Local Open Scope order_scope. Local Open Scope ring_scope. -Import Order.Theory Order.Def Order.Syntax GRing.Theory. +Import Order.TTheory Order.Def Order.Syntax GRing.Theory. Reserved Notation "<= y" (at level 35). Reserved Notation ">= y" (at level 35). @@ -5478,12 +5478,12 @@ Implicit Types x y z : R. Section MinMax. Definition minrC : @commutative R R min := @meetC _ R. Definition minrr : @idempotent R min := @meetxx _ R. -Definition minr_l x y : x <= y -> min x y = x := elimT meet_idPl. -Definition minr_r x y : y <= x -> min x y = y := elimT meet_idPr. +Definition minr_l x y : x <= y -> min x y = x := @meet_l _ _ x y. +Definition minr_r x y : y <= x -> min x y = y := @meet_r _ _ x y. Definition maxrC : @commutative R R max := @joinC _ R. Definition maxrr : @idempotent R max := @joinxx _ R. -Definition maxr_l x y : y <= x -> max x y = x := elimT join_idPr. -Definition maxr_r x y : x <= y -> max x y = y := elimT join_idPl. +Definition maxr_l x y : y <= x -> max x y = x := @join_l _ _ x y. +Definition maxr_r x y : x <= y -> max x y = y := @join_r _ _ x y. Definition minrA x y z : min x (min y z) = min (min x y) z := meetA x y z. Definition minrCA : @left_commutative R R min := meetCA. Definition minrAC : @right_commutative R R min := meetAC. @@ -5674,5 +5674,3 @@ Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] End Num. End mc_1_9. - -Export mc_1_9 mc_1_9.Num.Syntax. -- cgit v1.2.3