X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fconcrete_spaces.ma;h=5c39beddeee5d2895078095ad53c129ee05cc876;hb=45c7aae67e888fd4aa3ae03378cbcaeb4f5fdaf9;hp=4accb180381603cc35c0b3eb0fd2992bca7e8aef;hpb=7fad6f9727bb6f054c0198cf10354be4b355baef;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 4accb1803..5c39bedde 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -14,17 +14,139 @@
 
 include "formal_topology/basic_pairs.ma".
 
-interpretation "REL carrier" 'card c = (carrier c).
-
-definition comprehension: ∀b:REL. (b → CProp) → Ω \sup |b| ≝
- λb:REL.λP.{x | ∃p: x ∈ b. P (mk_ssigma ?? x p)}.
+definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
+ intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+qed.
 
 interpretation "subset comprehension" 'comprehension s p =
- (comprehension s p).
+ (comprehension s (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
+ apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (H‡#)); apply refl1
+  | intros; simplify; split; intros; simplify; intros;
+     [ apply (. #‡(#‡H)); assumption
+     | apply (. #‡(#‡H\sup -1)); assumption]]
+qed.
+
+definition BPext: ∀o: basic_pair. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+
+definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+ (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
+ intros (X S r); constructor 1;
+  [ intro F; constructor 1; constructor 1;
+    [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
+    | intros; split; intro; cases f (H1 H2); clear f; split;
+       [ apply (. (H‡#)); assumption
+       |3: apply (. (H\sup -1‡#)); assumption
+       |2,4: cases H2 (w H3); exists; [1,3: apply w]
+         [ apply (. (#‡(H‡#))); assumption
+         | apply (. (#‡(H \sup -1‡#))); assumption]]]
+  | intros; split; simplify; intros; cases f; cases H1; split;
+     [1,3: assumption
+     |2,4: exists; [1,3: apply w]
+      [ apply (. (#‡H)‡#); assumption
+      | apply (. (#‡H\sup -1)‡#); assumption]]]
+qed.
+
+definition BPextS: ∀o: basic_pair. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+ λo.extS ?? (rel o).
+
+definition fintersects: ∀o: basic_pair. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+ intros (o); constructor 1;
+  [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
+    intros; simplify; apply (.= (†H)‡#); apply refl1
+  | intros; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
+
+definition fintersectsS:
+ ∀o:basic_pair. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ intros (o); constructor 1;
+  [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+    intros; simplify; apply (.= (†H)‡#); apply refl1
+  | intros; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
+
+definition relS: ∀o: basic_pair. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+ intros (o); constructor 1;
+  [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
+  | intros; split; intros; cases H2; exists [1,3: apply w]
+     [ apply (. (#‡H1)‡(H‡#)); assumption
+     | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+qed.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
+
+record concrete_space : Type ≝
+ { bp:> basic_pair;
+   converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+   all_covered: ∀x: concr bp. x ⊩ form bp
+ }.
+
+(*
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> relation_pair CS1 CS2;
+   respects_converges:
+    ∀b,c.
+     extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
+     extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+   respects_all_covered:
+    extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
+    extS ?? (rel CS1) (form CS1)
+ }.
+
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+ intros;
+ constructor 1;
+  [ apply (convergent_relation_pair c c1)
+  | constructor 1;
+     [ intros;
+       apply (relation_pair_equality c c1 c2 c3);
+     | intros 1; apply refl;
+     | intros 2; apply sym; 
+     | intros 3; apply trans]]
+qed.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
+ intros;
+ unfold extS;
+ split;
+  [ intros 2;
+    cases m; clear m;
+    cases H; clear H;
+    cases H1; clear H1;
+    whd in H;
+    apply (eq_elim_r'' ????? H);
+    assumption
+  | intros 2;
+    constructor 1;
+     [ whd; exact I 
+     | exists; [ apply a ]
+       split;
+        [ assumption
+        | whd; constructor 1]]]
+qed.
 
-definition ext: ∀o: basic_pair. (form o) → Ω \sup |(concr o)| ≝
- λo,f.{x ∈ (concr o) | x ♮(rel o) f}.
+definition CSPA: category.
+ constructor 1;
+  [ apply concrete_space
+  | apply convergent_relation_space_setoid
+  | intro; constructor 1;
+     [ apply id
+     | intros;
+       unfold id; simplify;
+       apply (.= (equalset_extS_id_X_X ??));
 
-definition downarrow ≝
- λo: basic_pair.λa,b: form o.
-  {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
\ No newline at end of file
+     |
+     ]
+  |*)
\ No newline at end of file