From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Sep 2008 11:56:03 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4818
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=80c5d1841a5ea1d302f9b6865a6f1539d9361524;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 89665e5f9..568f3c052 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -56,15 +56,19 @@ definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o)
 qed.
 
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
-(*
-definition fintersectsS ≝
- λo: basic_pair.λa,b: Ω \sup (form o).
-  {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b }.
+
+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.
+qed.
 
 interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
 
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
- λo,x,S. ∃y.y ∈ S ∧ x ⊩ y.
+(*
+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 ∧ x ⊩ y);
 
 interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).