more notation

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

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 03da27c41cd71adc3e7e18a9c6156b178522b139..4228e64501cbdc0da61c1b05a9bf6c358b2392e1 100644 (file)
--- 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 *)