Major reordering of theorems in the appropriate files.

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

diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
index 62b11676a7571bf9b07092fee62e2a36e14326ff..ba2d65ba0cb32dfe84fd3d47f248eb1289652930 100644 (file)
--- a/helm/software/matita/library/formal_topology/formal_topologies.ma
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -60,10 +60,15 @@ interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U
 
 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);
+   C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
    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);
@@ -74,12 +79,18 @@ 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 ≝
+definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
  λFT1,FT2,c.cr ?? c.
 
-coercion cr'.
+coercion cr''.
 
 (*
+theorem 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.
+ intros;
+qed.
+
 definition formal_map_composition:
  ∀o1,o2,o3: formal_topology.
   binary_morphism1
@@ -90,4 +101,7 @@ definition formal_map_composition:
   [ intros; whd in c c1; constructor 1;
      [ apply (comp1 BTop ??? c c1);
      | intros;
+       apply (.= (extS_com ??? c c1 ?));
+       apply (.= †(C1 ?????));
+       apply (.= (C1 ?????));
 *)
\ No newline at end of file