From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Sep 2008 19:55:56 +0000 (+0000)
Subject: formal_map now defined
X-Git-Tag: make_still_working~4778
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7fb962ce66388785d27e699d921aa7b03a170139;p=helm.git

formal_map now defined
---

diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
index 5483dfa37..d6bcf4dda 100644
--- a/helm/software/matita/library/datatypes/subsets.ma
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -116,12 +116,15 @@ qed.
 
 interpretation "union" 'union U V = (fun1 ___ (union _) U V).
 
-definition singleton: ∀A:setoid. A → Ω \sup A.
- apply (λA:setoid.λa:A.{b | a=b});
- intros; simplify;
- split; intro;
- apply (.= H1);
-  [ apply H | apply (H \sup -1) ]
+definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
+ intros; constructor 1;
+  [ apply (λA:setoid.λa:A.{b | a=b});
+    intros; simplify;
+    split; intro;
+    apply (.= H1);
+     [ apply H | apply (H \sup -1) ]
+  | intros; split; intros 2; simplify in f ⊢ %; apply trans;
+     [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (singleton _ a).
+interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
\ No newline at end of file
diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
index e29ba16f7..2acb5642d 100644
--- a/helm/software/matita/library/formal_topology/formal_topologies.ma
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -24,7 +24,7 @@ coercion btop_carr'.
 
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
-  [ apply (λU:Ω \sup S.{a | ∃b. b ∈ U ∧ a ∈ A ? (singleton ? b)});
+  [ 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;
@@ -41,7 +41,25 @@ qed.
 
 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
 
-record formal_topology : Type ≝
+record formal_topology: Type ≝
  { bt:> BTop;
    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;
+  [ 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 S T;
+   C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
+   C2: extS ?? cr T = S
  }.
\ No newline at end of file