after a PITA, lebergue is dualized!

[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 a89a42ba81de31ba5d771c2378a923efad6b81c1..759037124310076d813c711ea272eb323d2d6ffc 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -15,24 +15,23 @@
 include "supremum.ma".
 
 (* Definition 2.13 *)
-alias symbol "square" = "bishop set square".
 alias symbol "pair" = "Pair construction".
 alias symbol "exists" = "exists".
 alias symbol "and" = "logical and".
 definition compose_bs_relations ≝
-  λC:bishop_set.λU,V:C square → Prop.
-   λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
+  λ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 square → Prop.
-   λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
+  λC:ordered_set.λU,V:C squareB → Prop.
+   λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
    
 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_bs_relation ≝
-  λC:bishop_set.λU:C square → Prop.
-    λx:C square. U 〈\snd x,\fst x〉.
+  λ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).
@@ -46,14 +45,14 @@ 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 *)