...

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

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 82278eb08823e394bcfcbb23024f0e8206306175..a89a42ba81de31ba5d771c2378a923efad6b81c1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -14,7 +14,6 @@
 
 include "supremum.ma".
 
-
 (* Definition 2.13 *)
 alias symbol "square" = "bishop set square".
 alias symbol "pair" = "Pair construction".
@@ -34,11 +33,8 @@ interpretation "ordered set relations composition" 'compose a b = (compose_os_re
 definition invert_bs_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈\snd x,\fst x〉.
-    
-notation < "s \sup (-1)"  with precedence 70 for @{ 'invert $s }.
-notation < "s \sup (-1) x"  with precedence 70
-  for @{ 'invert_appl $s $x}. 
-notation > "'inv'" with precedence 70 for @{ 'invert_symbol  }.
+      
+notation > "\inv" with precedence 60 for @{ 'invert_symbol  }.
 interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
@@ -57,7 +53,7 @@ record uniform_space : Type ≝ {
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
   us_phi3: ∀U:us_carr square → Prop. us_unifbase U → 
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
-  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
+  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
 }.
 
 (* Definition 2.14 *)  
@@ -66,9 +62,9 @@ definition cauchy ≝
   λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → 
    ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
    
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 
+notation < "a \nbsp 'is_cauchy'" non associative with precedence 45 
   for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 50 
+notation > "a 'is_cauchy'" non associative with precedence 45 
   for @{'cauchy $a}.
 interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
    
@@ -77,9 +73,9 @@ definition uniform_converge ≝
   λC:uniform_space.λa:sequence C.λu:C.
     ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U 〈u,a i〉.
     
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
+notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
   for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 50 
+notation > "a 'uniform_converges' x" non associative with precedence 45 
   for @{'uniform_converge $a $x}.
 interpretation "Uniform convergence" 'uniform_converge s u =
  (uniform_converge _ s u).