X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Frelations.ma;h=789f312cf0260da24d333203d898af38a3abca3f;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=1503fa5dec6996670e1d5ec0fcbf6de0fbde1849;hpb=13088dbb8e54833dfbe2d6c38b08d78fc36452a8;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 1503fa5de..789f312cf 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -140,25 +140,24 @@ definition ext: ∀X,S:REL. (X ⇒_\r1 S) × S ⇒_1 (Ω^X).
        apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
 qed.
 
-(*
-definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+definition extS: ∀X,S:REL. ∀r:X ⇒_\r1 S. Ω^S ⇒_1 Ω^X.
  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
  intros (X S r); constructor 1;
   [ intro F; constructor 1; constructor 1;
     [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
     | intros; split; intro; cases f (H1 H2); clear f; split;
-       [ apply (. (H‡#)); assumption
-       |3: apply (. (H\sup -1‡#)); assumption
+       [ apply (. (e^-1‡#)); assumption
+       |3: apply (. (e‡#)); assumption
        |2,4: cases H2 (w H3); exists; [1,3: apply w]
-         [ apply (. (#‡(H‡#))); assumption
-         | apply (. (#‡(H \sup -1‡#))); assumption]]]
-  | intros; split; simplify; intros; cases f; cases H1; split;
+         [ apply (. (#‡(e^-1‡#))); assumption
+         | apply (. (#‡(e‡#))); assumption]]]
+  | intros; split; simplify; intros; cases f; cases e1; split;
      [1,3: assumption
      |2,4: exists; [1,3: apply w]
-      [ apply (. (#‡H)‡#); assumption
-      | apply (. (#‡H\sup -1)‡#); assumption]]]
+      [ apply (. (#‡e^-1)‡#); assumption
+      | apply (. (#‡e)‡#); assumption]]]
 qed.
-
+(*
 lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
  intros;
  unfold extS; simplify;
@@ -251,9 +250,11 @@ definition minus_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U).
     [ apply (. e^-1 a2 w); | apply (. e a2 w)] assumption;]
 qed.
 
-interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) r).
-interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) r).
-interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) r).
+definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x.
+
+interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) (foo ?? r)).
+interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) (foo ?? r)).
+interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) (foo ?? r)).
 
 definition image_coercion: ∀U,V:REL. (U ⇒_\r1 V) → Ω^U ⇒_2 Ω^V.
 intros (U V r Us); apply (image U V r); qed.
@@ -271,7 +272,8 @@ theorem image_id: ∀o. (id1 REL o : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o
     exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]]
 qed.
 
-theorem minus_star_image_id: ∀o:REL. (fun12 ?? (minus_star_image o o) (id1 REL o) : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
+theorem minus_star_image_id: ∀o:REL. 
+  ((id1 REL o)⎻* : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
  intros; unfold minus_star_image; simplify; intro U; simplify; 
  split; simplify; intros;
   [ change with (a ∈ U); apply f; change with (a=a); apply refl1
@@ -296,6 +298,7 @@ theorem minus_star_image_comp:
  | cases f1; cases x1; apply f; assumption]
 qed.
 
+
 (*
 (*CSC: unused! *)
 theorem ext_comp:
@@ -311,13 +314,13 @@ theorem ext_comp:
   | cases H; clear H; cases x1; clear x1; exists [apply w]; split;
      [2: cases f] assumption]
 qed.
+*)
+
+axiom daemon : False.
 
 theorem extS_singleton:
- ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
+ ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x. 
  intros; unfold extS; unfold ext; unfold singleton; simplify;
- split; intros 2; simplify; cases f; split; try assumption;
-  [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
-    assumption
-  | exists; try assumption; split; try assumption; change with (x = x); apply refl]
-qed.
-*)
+ split; intros 2; simplify; simplify in f; 
+ [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file