one line

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

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 ≝