From 7fad6f9727bb6f054c0198cf10354be4b355baef Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Aug 2008 09:37:21 +0000
Subject: [PATCH] Better notation, in particular for subset comprehension.

---
 helm/software/matita/core_notation.moo        |  6 ++++
 .../formal_topology/concrete_spaces.ma        | 30 +++++++++++++++++++
 .../library/formal_topology/relations.ma      | 17 ++++++++++-
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 helm/software/matita/library/formal_topology/concrete_spaces.ma

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index f8bacd108..cceee2412 100644
--- 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
index 000000000..4accb1803
--- /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 2386a34d4..e67b2ce7c 100644
--- 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.
-- 
2.39.2