one line

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 78372e72fc6e2394234451fd10f8e30b5728cdb7..4c61f0fb47753fc191b383a9f74bff27c0d718de 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -66,7 +66,7 @@ record OAlgebra : Type := {
   oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
-  oa_overlap_preservers_meet: 
+  oa_overlap_preservers_meet_: 
       ∀p,q.oa_overlap p q → oa_overlap p 
        (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
   oa_join_split:
@@ -89,19 +89,41 @@ notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\
 non associative with precedence 50 for @{ 'oa_meet $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+
+(*
 notation < "hovbox(a ∧ b)" left associative with precedence 35
 for @{ 'oa_meet_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-
+*)
 notation > "hovbox(∧ f)" non associative with precedence 60
 for @{ 'oa_meet $f }.
+(*
 notation > "hovbox(a ∧ b)" left associative with precedence 50
 for @{ 'oa_meet (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
-
+*)
 interpretation "o-algebra meet" 'oa_meet f = 
   (fun_1 __ (oa_meet __) f).
 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
   (fun_1 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
 
+definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q); 
+  apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; apply (prop_1 ?? (oa_meet O BOOL)); intro x; simplify;
+  cases x; simplify; assumption;]
+qed.
+
+notation "hovbox(a ∧ b)" left associative with precedence 35
+for @{ 'oa_meet_bin $a $b }.
+interpretation "o-algebra binary meet" 'oa_meet_bin a b = 
+  (fun1 ___ (binary_meet _) a b).
+
+lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
+intros;  lapply (oa_overlap_preservers_meet_ O p q f);
+lapply (prop1 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+[3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
+qed.
+
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 49 for @{ 'oa_join $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index 633f0b89e01591db6d5c73c75800fa608ed50385..c2dc0fc60a0e4ddae9ecefd422526218775c138d 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -72,14 +72,27 @@ interpretation "o-concrete space downarrow" 'downarrow x =
 definition bp': concrete_space → basic_pair ≝ λc.bp c.
 coercion bp'.
 
+lemma setoid_OF_OA : OA → setoid.
+intros; apply (oa_P o);
+qed.
+
+coercion setoid_OF_OA.
+
+definition binary_downarrow : 
+  ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C).
+intros; constructor 1;
+[ intros; apply (↓ c ∧ ↓ c1);
+| intros; apply ((†H)‡(†H1));]
+qed.
+
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
  { rp:> arrows1 ? CS1 CS2;
    respects_converges:
-    ∀b,c.
+    ∀b,c. (rp\sub\c)⎻ (Ext⎽CS2 (b ↓ c)) = ?(*  
      extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
      BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
    respects_all_covered:
-    extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
+    extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)*)
  }.
 
 definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝