Major reordering of theorems in the appropriate files.

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a48eb164a822af5044ad648632000895b3557bbc..6fa8e35ad86df21bcad372561711315560c0ed52 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -93,15 +93,15 @@ definition strictly_increasing ≝
 definition strictly_decreasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
 
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 50 
+notation > "s 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
 interpretation "Ordered set strict increasing"  'strictly_increasing s    = 
   (strictly_increasing _ s).
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 50 
+notation > "s 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
   (strictly_decreasing _ s).
@@ -217,7 +217,7 @@ qed.
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
+     (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
@@ -227,13 +227,12 @@ notation > "a 'order_converges' x" non associative with precedence 45
 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
     
 (* Definition 2.8 *)
-alias symbol "and" = "constructive and".
 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
-notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
+notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
 interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
 
-notation "hvbox(x \in break [a,b])" non associative with precedence 45 
+notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45 
   for @{'segment_in $a $b $x}.
 interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).