...

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

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 729f2894b845b1414952e55342d1b851f6f86b75..92e9e975d79682b1f39dc3d3d96233a755ab7f25 100644 (file)
--- 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
@@ -27,34 +27,32 @@ 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 y ≝ (f⎻* ); clearbody y;
- change in y with (carr2 (POW (form s_1) ⇒ POW (form t_1)));
-alias symbol "Vdash" = "basic pair relation for subsets (non applied)".
-letin z ≝ (image ?? (⊩ \sub s_1)); clearbody z;
-change in z with ((POW (concr s_1) → POW (form s_1)));
- (*change in z with (carr2 (POW (concr s_1) ⇒ POW (form s_1)));*)
-
- letin R ≝ (y ∘ z);
-
- letin R ≝ (f* );∘ (⊩ \sub s_1));
-
-
-whd in ⊢ (? % ?→?); 
-whd in ⊢ (? % ?→?);  cases s_eq; intro; whd in f;
-simplify;
-intro; cases f (g H1 H2); clear f; exists;
- [ constructor 1;
-    [
-    | unfold F1; simplify;
-    |
-    ]
- |
+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));
+      | 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))));
+      | intros; unfold FunClass_1_OF_Ocontinuous_relation;
+        unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
+        apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
+    | whd; simplify; intros; split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
+      cases f1; clear f1; cases x1; clear x1;
+       [
+       | exists;
+       ]
  ]
 
- cases f (h H1 H2); clear f; simplify;
-change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with 
-  (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).
-
 STOP;