unary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations_to_o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 40db8183fc79464f39ec508abafa16ed33016054..781514e0757cfdbd2e33811ac1ba9f0c3d1c2210 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -52,7 +52,7 @@ definition SUBSETS: objs1 SET → OAlgebra.
           exists; [apply w] assumption]]
   | intros; intros 2; cases (f (singleton ? a) ?);
      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]
-     | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#));
+     | change in x1 with (a = w); change with (mem A a q); apply (. (x1‡#));
        assumption]]
 qed.
 
@@ -99,21 +99,21 @@ lemma orelation_of_relation_preserves_equality:
  intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
  simplify; whd in o1 o2;
   [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
-    apply (. #‡(e‡#));
+    apply (. #‡(e^-1‡#));
   | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a);
-    apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
     apply (. #‡(e‡#));
-  | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
+  | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
     apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
+  | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
     apply (. #‡(e‡#));
-  | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
+  | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
     apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
+  | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
     apply (. #‡(e‡#));
+  | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
+    apply (. #‡(e ^ -1‡#));
   | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a);
-    apply (. #‡(e ^ -1‡#)); ]
+    apply (. #‡(e‡#)); ]
 qed.
 
 lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
@@ -127,22 +127,22 @@ lemma orelation_of_relation_preserves_identity:
   [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;
   | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
-    change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f;
+    change in f1 with (x = a1); apply (. f1‡#); apply f;
   | alias symbol "and" = "and_morphism".
     change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
-    apply (. f^-1‡#); apply f1;
+    apply (. f‡#); apply f1;
   | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
   | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
-    apply (. f‡#); apply f1;
+    apply (. f^-1‡#); apply f1;
   | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
   | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;
   | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
-    change in f1 with (a1 = y); apply (. f1‡#); apply f;]
+    change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;]
 qed.
 
 lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T).