From 5796d0d7fdb89f06fecadbdc58541a886dca44cd Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Sep 2008 16:55:33 +0000
Subject: [PATCH] ...

---
 .../formal_topology/concrete_spaces.ma        | 64 ++++++++++---------
 1 file changed, 34 insertions(+), 30 deletions(-)

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 9885a6673..0248b72a1 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -30,6 +30,8 @@ definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
      | 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;
@@ -48,43 +50,45 @@ definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
       | apply (. (#‡H\sup -1)‡#); assumption]]]
 qed.
 
-definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
- apply
-  (λo: basic_pair.λa,b: form o.
-    {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
+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 = (fintersects _ U V).
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
 
 definition fintersectsS:
- ∀o:basic_pair. Ω \sup (form o) → Ω \sup (form o) → Ω \sup (form o).
- apply (λo: basic_pair.λa,b: Ω \sup (form o).
-  {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
+ ∀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 = (fintersectsS _ U V).
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
 
-(*
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
- 
-
- apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ 
-   (* OK: FunClass_2_OF_binary_relation (concr o) (form o) (rel o) x y *)
-   ?);
-   change in x with (carr1 (setoid1_of_setoid (concr o)));
-   apply (FunClass_2_OF_binary_relation ?? (rel ?) x y); 
-x ⊩ y);
- 
- rel (concr o) o -> binary_relation ...
- rel ? = seotid1_OF_setoid ?
- carr rel ? = Type_OF_objs1 (concr o) -> 
-         carr (setoid1_of_REL (concr o))
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
+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);
+     (* BUG HERE: WORKAROUND *) apply (concr o);
+  | 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 (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);
@@ -146,4 +150,4 @@ definition CSPA: category.
 
      |
      ]
-  |*)
+  |*)
\ No newline at end of file
-- 
2.39.2