...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_pairs_to_o-basic_topologies.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index b745652569c9458b389903f2a220c93c03c3d6f9..80fec034864530c78435b77e40daa82118e6ba10 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -64,30 +64,30 @@ definition o_continuous_relation_of_o_relation_pair:
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
-  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros (U e);
     apply sym1;
-    apply (.= †(†e));
-    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
-    cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
-      cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+    apply (.= †(†e)); 
+    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U));
+    cut ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U) = ((⊩) ∘ t \sub \c) ((⊩\sub BP1)* U)) as COM;[2:
+      cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩\sub BP1)* U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
-    apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+    apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩\sub BP1)* U))));
     apply (.= COM ^ -1);
-    change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+    change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩\sub BP1)* ) U));
     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
     apply (†e^-1);
   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
     apply (.= †(†e));
-    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
-    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
-      cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U));
+    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩\sub BP1)⎻ U)) as COM;[2:
+      cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩\sub BP1)⎻ U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
-    apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+    apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩\sub BP1)⎻ U))));
     apply (.= COM ^ -1);
-    change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+    change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩\sub BP1)⎻ ) U));
     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
     apply (†e^-1);]
 qed.