virtuals for () removed and bound to 'o'

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / subsets.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 7eb2d1e9423bc88f1026ccf38c1a3ac88193b8f7..3aaf2d3d6b34b6da73f52a678e6cfb7d95c5f73b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -12,12 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/cprop_connectives.ma".
 include "categories.ma".
 
 record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
 
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp1 ≝
+definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp0 ≝
  λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
 
 theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
@@ -140,4 +139,29 @@ definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
      [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (fun11 __ (singleton _) a).
\ No newline at end of file
+interpretation "singleton" 'singl a = (fun11 __ (singleton _) a).
+
+definition big_intersects:
+ ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+ intros; constructor 1;
+  [ intro; whd; whd in I;
+    apply ({x | ∀i:I. x ∈ t i});
+    simplify; intros; split; intros; [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
+    apply f;
+  | intros; split; intros 2; simplify in f ⊢ %; intro;
+     [ apply (. (#‡(e i))); apply f;
+     | apply (. (#‡(e i)\sup -1)); apply f]]
+qed.
+
+definition big_union:
+ ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+ intros; constructor 1;
+  [ intro; whd; whd in A; whd in I;
+    apply ({x | ∃i:carr I. x ∈ t i });
+    simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
+    [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
+    apply x;
+  | intros; split; intros 2; simplify in f ⊢ %; cases f; clear f; exists; [1,3:apply w]
+     [ apply (. (#‡(e w))); apply x;
+     | apply (. (#‡(e w)\sup -1)); apply x]]
+qed.