Convergence is now defined.

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index cceee24124153d236671b761b466f5af791afaa3..c6f66918d0ba74cc8fb2d384b70ae90fd503c825 100644 (file)
--- 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 3814ac3f1d138c77f5638ce922c34424ee9fe3b9..67f0ffa54deb3050a04b3347e0940eb6be373caa 100644 (file)
--- 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 4accb180381603cc35c0b3eb0fd2992bca7e8aef..ec32fca817fcc6723f51fc777d9c13a04b6b815b 100644 (file)
--- 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