X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fformal_topologies.ma;h=a611e22ea9d5620404f2045e597824001ab1b80a;hb=071d7a246190074c97e78192839e4bb5d5a1eef4;hp=eb2b0b1f730751d14401b6a95fbdd050b0d7a979;hpb=49045bfd9b3038ce30a1911e2345f949ed38ec8a;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
index eb2b0b1f7..a611e22ea 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
@@ -14,13 +14,6 @@
 
 include "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.
-
-coercion btop_carr'.
 
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
@@ -46,9 +39,6 @@ record formal_topology: Type ≝
    converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
  }.
 
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
 
 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  intros; constructor 1;
@@ -64,11 +54,6 @@ record formal_map (S,T: formal_topology) : Type ≝
    C2: extS ?? cr T = S
  }.
 
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  intros (S T); constructor 1;
   [ apply (formal_map S T);
@@ -79,16 +64,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1.
      | simplify; intros 3; apply trans1]]
 qed.
 
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
 axiom C1':
  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.