X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-formal_topologies.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-formal_topologies.ma;h=0000000000000000000000000000000000000000;hb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;hp=0e0b02e941c83bf98410a10e00c366a2d7d4f54f;hpb=05cfeb82d2624860e66941421a937f308d66cf33;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
deleted file mode 100644
index 0e0b02e94..000000000
--- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
+++ /dev/null
@@ -1,99 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "o-basic_topologies.ma".
-
-(*
-(*
-definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
- intros; constructor 1;
-  [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
-    intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
-    split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
-  | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
-    try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
-qed.
-
-interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
-
-definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
- intros; constructor 1;
-  [ apply (λU,V. ↓U ∩ ↓V);
-  | intros; apply (.= (†H)‡(†H1)); apply refl1]
-qed.
-
-interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
-*)
-
-record formal_topology: Type ≝
- { bt:> OBTop;
-   converges: ∀U,V: bt. oA bt (U ↓ V) = (oA ? U ∧ oA ? V)
- }.
-
-(*
-
-definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
- intros; constructor 1;
-  [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
-  | intros; apply (.= (†H)‡(†H1)); apply refl1]
-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;
-   C2: extS ?? cr T = S
- }.
-
-definition formal_map_setoid: formal_topology → formal_topology → setoid1.
- intros (S T); constructor 1;
-  [ apply (formal_map S T);
-  | constructor 1;
-     [ apply (λf,f1: formal_map S T.f=f1);
-     | simplify; intros 1; apply refl1
-     | simplify; intros 2; apply sym1
-     | simplify; intros 3; apply trans1]]
-qed.
-
-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.
-
-definition formal_map_composition:
- ∀o1,o2,o3: formal_topology.
-  binary_morphism1
-   (formal_map_setoid o1 o2)
-   (formal_map_setoid o2 o3)
-   (formal_map_setoid o1 o3).
- intros; constructor 1;
-  [ intros; whd in c c1; constructor 1;
-     [ apply (comp1 BTop ??? c c1);
-     | intros;
-       apply (.= (extS_com ??? c c1 ?));
-       apply (.= †(C1 ?????));
-       apply (.= (C1' ?????));
-       apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
-       apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
-       apply (.= (extS_singleton ????)‡(extS_singleton ????));
-       apply refl1;
-     | apply (.= (extS_com ??? c c1 ?));
-       apply (.= (†(C2 ???)));
-       apply (.= (C2 ???));
-       apply refl1;]
-  | intros; simplify;
-    change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
-    apply prop1; assumption]
-qed.
-*)