more notation

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

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 1806408e045afcda9e82509808f6a1a9675c737b..fdd226f0f974318569f5fb245b5e0fe4fcfff026 100644 (file)
--- 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;