X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fo-basic_pairs_to_o-basic_topologies.ma;h=fdd226f0f974318569f5fb245b5e0fe4fcfff026;hb=42705ef31dd3513a998533e02b5f20fb38dd4fb2;hp=1806408e045afcda9e82509808f6a1a9675c737b;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
index 1806408e0..fdd226f0f 100644
--- a/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
@@ -59,8 +59,8 @@ definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
 qed.
 
 definition o_continuous_relation_of_o_relation_pair:
- ∀BP1,BP2.arrows2 OBP BP1 BP2 →
-  arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
+ ∀BP1,BP2.BP1 ⇒_\obp2 BP2 →
+  (o_basic_topology_of_o_basic_pair BP1) ⇒_\obt2 (o_basic_topology_of_o_basic_pair BP2).
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
@@ -93,7 +93,7 @@ definition o_continuous_relation_of_o_relation_pair:
 qed.
 
 
-definition OR : carr3 (arrows3 CAT2 OBP OBTop).
+definition OR : carr3 (OBP ⇒_\c3 OBTop).
 constructor 1;
 [ apply o_basic_topology_of_o_basic_pair;
 | intros; constructor 1;