Better notation, in particular for subset comprehension.

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index f8bacd1086f19dd34962353a43bbda8cd43c640a..cceee24124153d236671b761b466f5af791afaa3 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -168,6 +168,12 @@ for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
 notation > "hvbox({ ident i | term 19 p })" with precedence 90
 for @{ 'subset (\lambda ${ident i}. $p)}.
 
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
 notation "hvbox(a break ∈ b)" non associative with precedence 45
 for @{ 'mem $a $b }.
 

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
new file mode 100644 (file)
index 0000000..4accb18
--- /dev/null
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "formal_topology/basic_pairs.ma".
+
+interpretation "REL carrier" 'card c = (carrier c).
+
+definition comprehension: ∀b:REL. (b → CProp) → Ω \sup |b| ≝
+ λb:REL.λP.{x | ∃p: x ∈ b. P (mk_ssigma ?? x p)}.
+
+interpretation "subset comprehension" 'comprehension s p =
+ (comprehension s p).
+
+definition ext: ∀o: basic_pair. (form o) → Ω \sup |(concr o)| ≝
+ λo,f.{x ∈ (concr o) | x ♮(rel o) f}.
+
+definition downarrow ≝
+ λo: basic_pair.λa,b: form o.
+  {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
\ No newline at end of file

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 2386a34d4a644244e2e26c77de2e4aa21687f8bd..e67b2ce7c5ea8792fd4b715efb3befe79dcaa2c5 100644 (file)
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -127,4 +127,19 @@ definition REL: category.
        [ rewrite > H | rewrite < H2 ]
        assumption
      |*: exists; try assumption; split; first [ reflexivity | assumption ]]]
-qed.
\ No newline at end of file
+qed.
+
+definition elements: objs REL → Type ≝
+ λb:ΣA.Ω\sup A.ssigma (s_witness ?? b) (s_proof ?? b).
+
+coercion elements.
+
+definition carrier: objs REL → Type ≝
+ λb:ΣA.Ω\sup A.s_witness ?? b.
+
+interpretation "REL carrier" 'card c = (carrier c).
+
+definition subset: ∀b:objs REL. Ω \sup (carrier b) ≝
+ λb:ΣA.Ω\sup A.s_proof ?? b.
+
+coercion subset.