...

[helm.git] / helm / software / matita / library / demo / formal_topology.ma

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 41c0d5c53cb2253fe4a9ea2e0deca0c275d89529..15da20a1132aae02cb7df0a5b457096402649eb2 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -158,13 +158,9 @@ qed.
 
 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 
-notation "↑a" with precedence 80 for @{ 'uparrow $a }.
-
 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 
-definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
-
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 
 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 
@@ -174,6 +170,5 @@ interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-