From 9be608d0e7ae483754f9922ab521802288d6abf3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Aug 2008 14:45:44 +0000
Subject: [PATCH] Convergence is now defined.

---
 helm/software/matita/core_notation.moo          |  2 ++
 .../matita/library/demo/formal_topology.ma      |  2 --
 .../library/formal_topology/concrete_spaces.ma  | 17 ++++++++++++++---
 3 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index cceee2412..c6f66918d 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -201,6 +201,8 @@ notation "hvbox(a break \circ b)"
   left associative with precedence 55
 for @{ 'compose $a $b }.
 
+notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
+
 notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
 notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
 notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}. 
diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 3814ac3f1..67f0ffa54 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -149,8 +149,6 @@ interpretation "downarrow" 'downarrow a = (downarrow _ a).
 
 definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
-notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
-
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
 record convergent_generated_topology : Type ≝
diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 4accb1803..ec32fca81 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -22,9 +22,20 @@ definition comprehension: ∀b:REL. (b → CProp) → Ω \sup |b| ≝
 interpretation "subset comprehension" 'comprehension s p =
  (comprehension s p).
 
-definition ext: ∀o: basic_pair. (form o) → Ω \sup |(concr o)| ≝
+definition ext: ∀o: basic_pair. form o → Ω \sup |(concr o)| ≝
  λo,f.{x ∈ (concr o) | x ♮(rel o) f}.
 
-definition downarrow ≝
+definition fintersects ≝
  λo: basic_pair.λa,b: form o.
-  {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
\ No newline at end of file
+  {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
+
+interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+
+definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
+ λo,x,S. ∃y. 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 _).
+
+definition convergence ≝
+ λo: basic_pair.∀a: concr o.∀U,V: form o. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V). 
\ No newline at end of file
-- 
2.39.2