1) as usual, I took the reverse notation for composition.

[helm.git] / helm / software / matita / library / formal_topology / concrete_spaces.ma

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index d95072cb973a2fa4c65f3ecd60212f84ba71438a..3c03b4e667803df8815c98e4ef7806ae86b47715 100644 (file)
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -67,23 +67,23 @@ definition convergent_relation_space_composition:
        constructor 1;
         [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
         | intros;
-          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
-            with (c \sub \f ∘ c1 \sub \f);
+            with (c1 \sub \f ∘ c \sub \f);
           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
-            with (c \sub \f ∘ c1 \sub \f);
+            with (c1 \sub \f ∘ c \sub \f);
           apply (.= (extS_com ??????));
           apply (.= (†(respects_converges ?????)));
           apply (.= (respects_converges ?????));
           apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
           apply refl1;
-        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
           apply (.= (extS_com ??????));
           apply (.= (†(respects_all_covered ???)));
           apply (.= respects_all_covered ???);
           apply refl1]
      | intros;
-       change with (a ∘ b = a' ∘ b');
+       change with (b ∘ a = b' ∘ a');
        change in H with (rp'' ?? a = rp'' ?? a');
        change in H1 with (rp'' ?? b = rp ?? b');
        apply (.= (H‡H1));
@@ -106,15 +106,15 @@ definition CSPA: category1.
        apply refl1]
   | apply convergent_relation_space_composition
   | intros; simplify;
-    change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+    change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
     apply (.= ASSOC1);
     apply refl1
   | intros; simplify;
-    change with (id1 ? o1 ∘ a = a);
-    apply (.= id_neutral_left1 ????);
+    change with (a ∘ id1 ? o1 = a);
+    apply (.= id_neutral_right1 ????);
     apply refl1
   | intros; simplify;
-    change with (a ∘ id1 ? o2 = a);
-    apply (.= id_neutral_right1 ????);
+    change with (id1 ? o2 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
     apply refl1]
 qed.