X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-formal_topologies.ma;h=4b667546b0179efe84950ae67e057a3c27dd3137;hb=cdc1636c7b536f1e667a2418140b82be6f4e0e30;hp=1693b55f61eb62677243c92d2e0a61380477adac;hpb=6e75e2415b0433a134e0050d63d627a66efea7a4;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
index 1693b55f6..4b667546b 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
@@ -12,13 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "o-concrete_spaces.ma".
+include "o-basic_topologies.ma".
 
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
-
-coercion btop_carr.
-
-definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
+(*
+definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
 
 coercion btop_carr'.
 
@@ -40,12 +37,14 @@ definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω
 qed.
 
 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+*)
 
 record formal_topology: Type ≝
  { bt:> BTop;
-   converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
+   converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
  }.
 
+(*
 definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
 
 coercion bt'.
@@ -57,7 +56,7 @@ definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
 qed.
 
 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
-
+*)
 record formal_map (S,T: formal_topology) : Type ≝
  { cr:> continuous_relation_setoid S T;
    C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;