use named types to force some constraints asap

[helm.git] / helm / software / matita / contribs / formal_topology / o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/o-algebra.ma b/helm/software/matita/contribs/formal_topology/o-algebra.ma
index 2c2a60171e310c0a637ce9b60f9b057558bd4142..dadca0e4c02676d813e7b6372d912144e912cc6b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/o-algebra.ma
@@ -35,7 +35,7 @@ record OAlgebra : Type := {
   oa_overlap_preservers_meet: 
     ∀p,q.oa_overlap p q → oa_overlap p (oa_meet bool (λx.match x with [ true ⇒ p | false ⇒ q ]));
   oa_join_split: 
-    ∀I.∀p,q_i.oa_overlap p (oa_join I q_i) ↔ ∃i:I.oa_overlap p (q_i i);
+    ∀I.∀p,q.oa_overlap p (oa_join I q) ↔ ∃i:I.oa_overlap p (q i);
   oa_density: 
     ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q    
 }.
@@ -50,18 +50,34 @@ notation > "hovbox(a ∧ b)" left associative with precedence 50
 for @{ 'oa_meet (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
 notation > "hovbox(∧ f)" non associative with precedence 60
 for @{ 'oa_meet $f }.
-notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \sub(ident i ∈ I) break p)" non associative with precedence 50
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
-notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \nbsp p)" non associative with precedence 50
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
 notation < "hovbox(a ∧ b)" left associative with precedence 50
-for @{ 'oa_meet (λx__:$_.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+for @{ 'oa_meet (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 
 interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
-include "nat/nat.ma".  
 
-lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A. (x ∧ y >< x) → x = ∧ (λi:ℕ.x) ∧ ∧ f.  
-  
+notation > "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+notation > "hovbox(∨ f)" non associative with precedence 59
+for @{ 'oa_join $f }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}:$I.$p) }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}.($p $_)) }.
+notation < "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
+
+interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
 
-notation ""
 
+include "nat/plus.ma".
+
+lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A.
+   x ≤ y → 
+   (x ∧ y >< x ∨ y ∧ x) → 
+   x = ∧ (λi:ℕ.x ∧ f i) ∧ ∨ (λi:ℕ.∧ (λx.f (x+i))) → x = y.
+intros;  
+