X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fo-basic_topologies.ma;h=4228e64501cbdc0da61c1b05a9bf6c358b2392e1;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=03da27c41cd71adc3e7e18a9c6156b178522b139;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_topologies.ma
index 03da27c41..4228e6450 100644
--- a/helm/software/matita/library/formal_topology/o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_topologies.ma
@@ -157,6 +157,11 @@ definition Ocontinuous_relation_setoid_of_arrows2_OBTop :
   ∀P,Q. arrows2 OBTop P Q → Ocontinuous_relation_setoid P Q ≝ λP,Q,x.x.
 coercion Ocontinuous_relation_setoid_of_arrows2_OBTop.
 
+notation > "B ⇒_\obt2 C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+notation "B ⇒\sub (\obt 2) C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+interpretation "'arrows2_OBT" 'arrows2_OBT A B = (arrows2 OBTop A B).
+
+
 (*
 (*CSC: unused! *)
 (* this proof is more logic-oriented than set/lattice oriented *)