X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Frelations.ma;h=5e2274047031ecc5cc02f2fc12c07f4b0d7d47de;hb=121d6d7cd72ae57a4ed838ef02ae98f3bafb6e9d;hp=e9989d4f76cbdd5df81b9e76c1e311f54c098865;hpb=da03907a38982b8b45459213f2b9581accac5143;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index e9989d4f7..5e2274047 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -98,4 +98,71 @@ coercion full_subset.
 
 definition setoid1_of_REL: REL → setoid ≝ λS. S.
 
-coercion setoid1_of_REL.
\ No newline at end of file
+coercion setoid1_of_REL.
+
+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 (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (H‡#)); apply refl1
+  | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
+     [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
+     | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
+qed.
+
+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.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
+ intros;
+ unfold extS; simplify;
+ split; simplify;
+  [ intros 2; change with (a ∈ X);
+    cases f; clear f;
+    cases H; clear H;
+    cases x; clear x;
+    change in f2 with (eq1 ? a w);
+    apply (. (f2\sup -1‡#));
+    assumption
+  | intros 2; change in f with (a ∈ X);
+    split;
+     [ whd; exact I 
+     | exists; [ apply a ]
+       split;
+        [ assumption
+        | change with (a = a); apply refl]]]
+qed.
+
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+ intros; unfold extS; simplify; split; intros; simplify; intros;
+  [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
+    exists; [apply w1] split [2: assumption] constructor 1; [assumption]
+    exists; [apply w] split; assumption
+  | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
+    cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
+    assumption]
+qed.
+