X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=15da20a1132aae02cb7df0a5b457096402649eb2;hb=01001c883a8151edba81cd03a6f254d24a81c867;hp=67f0ffa54deb3050a04b3347e0940eb6be373caa;hpb=9be608d0e7ae483754f9922ab521802288d6abf3;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 67f0ffa54..15da20a11 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -12,7 +12,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "datatypes/subsets.ma".
+include "logic/equality.ma".
+include "logic/cprop_connectives.ma".
+
+record powerset (A : Type) : Type ≝ { char : A → CProp }.
+
+interpretation "char" 'subset p = (mk_powerset _ p).  
+
+interpretation "pwset" 'powerset a = (powerset a). 
+
+interpretation "in" 'mem a X = (char _ X a). 
+
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
+
+interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
+
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
+
+interpretation "overlaps" 'overlaps u v = (overlaps _ u v).
+
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect _ u v). 
 
 record axiom_set : Type ≝ { 
   A:> Type;
@@ -108,12 +129,12 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
  generalize in match H; clear H; 
  apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
  clear H1; simplify; intros;
-  [ exists [apply a1] assumption
+  [ exists [apply x] assumption
   | cases H2 in j H H1; clear H2 a1; intros; 
     cases (H1 i); clear H1; apply (H3 a1); assumption]
 qed.
 
-definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 
 interpretation "covered by one" 'leq a b = (leq _ a b).
 
@@ -137,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).
 
@@ -153,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)
  }.
-