X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fr-o-basic_pairs.ma;h=72c5fe02d603608d30a73bbb87ce07e29c119f8b;hb=982eb9392e7fd9ee26a4ebf593244e8125ed7853;hp=1dcc1b91fe3c8a1c45746453190a1c16151c5faa;hpb=427bbecb65191dc43037c8d62dbdebeccf7c1c29;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 1dcc1b91f..72c5fe02d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -20,10 +20,47 @@ definition rOBP ≝ Apply ?? BP_to_OBP.
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
 lemma rOR_full : 
-  ∀rS,rT:rOBP.∀f:arrows2 BTop (OR (ℱ_2 rS)) (OR (ℱ_2 rT)).
-    exT22 ? (λg:arrows2 rOBP rS rT.
+  ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
+    exT22 ? (λg:arrows2 rOBP s t.
        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intros; cases f (c H1 H2); simplify;
+intro; cases s (s_2 s_1 s_eq); clear s; cases s_eq; clear s_eq s_2;
+intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
+whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
+intro; whd in s_1 t_1;
+letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
+ [2:
+   exists;
+    [ constructor 1;
+       [2: simplify; apply R;
+       | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
+       | simplify; apply rule #; ]]
+   simplify;
+ | constructor 1;
+    [2: constructor 1; constructor 1;
+      [ intros (x y); apply (y ∈ f (singleton ? x));
+      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+        unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
+        apply rule #; ]
+    |1: constructor 1; constructor 1;
+      [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
+      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+        unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
+        apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
+    | whd; simplify; intros; simplify;
+      whd in ⊢ (? % %); simplify in ⊢ (? % %);
+      lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
+       [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin;
+         lapply (s y); clear s;
+whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
+whd in Hletin; simplify in Hletin;
+         lapply (s1 y); clear s1;      
+     split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
+      cases f1; clear f1; cases x1; clear x1;
+       [
+       | exists;
+       ]
+ ]
+
 STOP;