X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fsubsets.ma;h=95d0284dc05ccc5397688f29c3cd26fefc60ae68;hb=1470ff47df1349333c6b721a1c162cc7dfc6806f;hp=8eedb552351134f7a9320fd6bdf88a4f2149e860;hpb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 8eedb5523..95d0284dc 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -17,7 +17,7 @@ include "categories.ma".
 record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }.
 interpretation "powerset low" 'powerset A = (powerset_carrier A).
 notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
-interpretation "memlow" 'mem_low a S = (mem_operator ? S a).
+interpretation "memlow" 'mem_low a S = (fun11 ?? (mem_operator ? S) a).
 
 definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp0 ≝
  λA:objs1 SET.λU,V.∀a:A. a ∈. U → a ∈. V.
@@ -162,3 +162,20 @@ definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
      [ apply (. (#‡(e w)^-1)); apply x;
      | apply (. (#‡e w)); apply x]]
 qed.
+
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (\emsp) term 90 p)" 
+non associative with precedence 50 for @{ 'bigcup $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (ident i ∈  I) break term 90 p)" 
+non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }.
+
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (\emsp) term 90 p)" 
+non associative with precedence 50 for @{ 'bigcap $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (ident i ∈  I) break term 90 p)" 
+non associative with precedence 50 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋂ f)" non associative with precedence 60 for @{ 'bigcap $f }.
+
+interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
+interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
+interpretation "bigcup mk" 'bigcup_mk f = (fun12 ?? (big_union ??) (mk_unary_morphism2 ?? f ?)).
+interpretation "bigcap mk" 'bigcap_mk f = (fun12 ?? (big_intersects ??) (mk_unary_morphism2 ?? f ?)).