X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs_to_o-basic_topologies.ma;h=b745652569c9458b389903f2a220c93c03c3d6f9;hb=3e5c359c75874748cfed8a9046031b62396e0e6d;hp=1bf31881c29d11fc3b0b1ddb90d96908efd3e552;hpb=b47c73ebbc1a6e8cc930a6c8c99f90d4fe2f19b8;p=helm.git

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 1bf31881c..b74565256 100644
--- 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
@@ -23,8 +23,8 @@ definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
  intro t;
  constructor 1;
   [ apply (Oform t);
-  | apply (□_t ∘ Ext⎽t);
-  | apply (◊_t ∘ Rest⎽t);
+  | apply (□⎽t ∘ Ext⎽t);
+  | apply (◊⎽t ∘ Rest⎽t);
   | apply hide; intros 2; split; intro;
      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
@@ -38,7 +38,7 @@ definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
           apply (. (or_prop2 : ?) ^ -1);
           apply oa_leq_refl; ]]
   | apply hide; intros 2; split; intro;
-     [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
+     [ change with (◊⎽t ((⊩) \sup * U) ≤ ◊⎽t ((⊩) \sup * V));
        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
        apply f_star_image_monotone;
@@ -51,7 +51,7 @@ definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
           apply oa_leq_refl; ]]
   | apply hide; intros;
     apply (.= (oa_overlap_sym' : ?));
-    change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
+    change with ((◊⎽t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊⎽t ((⊩)* V))));
     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
     apply (.= #‡(lemma_10_3_a : ?));
     apply (.= (or_prop3 : ?)^-1);