Concrete spaces now defined.

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index e179fe3f0695f3a6c541e177b82972fa16fc449b..5c39beddeee5d2895078095ad53c129ee05cc876 100644 (file)
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -76,19 +76,24 @@ qed.
 
 interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
 
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
- λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y.
+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 ___ (relS _) x y).
+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:
@@ -100,7 +105,6 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
     extS ?? (rel CS1) (form CS1)
  }.
 
-(*
 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
  intros;
  constructor 1;
@@ -145,4 +149,4 @@ definition CSPA: category.
 
      |
      ]
-  |*)
+  |*)
\ No newline at end of file