some work on duality, still not finisched

[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 b8b77572b67a4f4646a73b44091521018c0287bb..759037124310076d813c711ea272eb323d2d6ffc 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -15,67 +15,44 @@
 include "supremum.ma".
 
 (* Definition 2.13 *)
-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (pair S S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
-    [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
-    |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-notation "a \subseteq u" left associative with precedence 70 
-  for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b = (subset _ a b). 
-
-notation < "s  2 \atop \neq" non associative with precedence 90
-  for @{ 'square2 $s }.
-notation > "s 'square'" non associative with precedence 90
-  for @{ 'square $s }.
-interpretation "bishop set square" 'square x = (square_bishop_set x).    
-interpretation "bishop set square" 'square2 x = (square_bishop_set x).    
-
+alias symbol "pair" = "Pair construction".
 alias symbol "exists" = "exists".
 alias symbol "and" = "logical and".
-definition compose_relations ≝
-  λC:bishop_set.λU,V:C square → Prop.
-   λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+definition compose_bs_relations ≝
+  λC:bishop_set.λU,V:C squareB → Prop.
+   λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
+   
+definition compose_os_relations ≝
+  λC:ordered_set.λU,V:C squareB → Prop.
+   λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
    
-notation "a \circ b"  left associative with precedence 70
-  for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b = (compose_relations _ a b).
+interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
+interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
 
-definition invert_relation ≝
-  λC:bishop_set.λU:C square → Prop.
-    λx:C square. U 〈snd x,fst x〉.
-    
-notation < "s \sup (-1)"  left associative with precedence 70
-  for @{ 'invert $s }.
-notation < "s \sup (-1) x"  left associative with precedence 70
-  for @{ 'invert2 $s $x}. 
-notation > "'inv'" right associative with precedence 70
-  for @{ 'invert0  }.
-interpretation "relation invertion" 'invert a = (invert_relation _ a).
-interpretation "relation invertion" 'invert0 = (invert_relation _).
-interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
+definition invert_bs_relation ≝
+  λC:bishop_set.λU:C squareB → Prop.
+    λx:C squareB. U 〈\snd x,\fst x〉.
+      
+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).
 
 alias symbol "exists" = "CProp exists".
+alias symbol "compose" = "bishop set relations composition".
 alias symbol "and" (instance 21) = "constructive and".
 alias symbol "and" (instance 16) = "constructive and".
 alias symbol "and" (instance 9) = "constructive and".
 record uniform_space : Type ≝ {
   us_carr:> bishop_set;
-  us_unifbase: (us_carr square → Prop) → CProp;
-  us_phi1: ∀U:us_carr square → Prop. us_unifbase U → 
-    (λx:us_carr square.fst x ≈ snd x) ⊆ U;
-  us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
-    ∃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_unifbase: (us_carr squareB → Prop) → CProp;
+  us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U → 
+    (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
+  us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
+    ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
+  us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U → 
+    ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
+  us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
 }.
 
 (* Definition 2.14 *)  
@@ -84,9 +61,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).  
    
@@ -95,9 +72,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).