X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Fcantor.ma;h=6a79dd2d808df2478f6a4ad25568e41e1eb68894;hb=f5ca06e7437c022413b14bd8f63fa3466a1ead0c;hp=d3dccb8ee07e66248e17e69f21536cc6fb3013fe;hpb=1439ced76cb62f9c5f5e638c53a005c3843870ae;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index d3dccb8ee..6a79dd2d8 100644
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -78,7 +78,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ axs  
   (* -------------- *) ⊢
-         S x ≡ A. 
+         S (uax x) ≡ A. (* XXX: bug coercions/ disamb multipasso che ne fa 1 solo*) 
 
 ntheorem col2_4 :
   ∀A:uAx.∀a:uax A. a ◃ ∅ → ¬ a ∈ 𝐂 a one.
@@ -88,7 +88,8 @@ ntheorem col2_4 :
 ##]
 nqed.
 
-ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
+(* bug interpretazione non aggiunta per ∅ *)
+ndefinition Z : Ω^axs ≝ { x | x ◃ (emptyset ?) }.
 
 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
 #A; #a; #U; #V; #HUV; #H; nelim H; /3/; 
@@ -126,7 +127,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ caxs  
   (* -------------- *) ⊢
-         S x ≡ nat. 
+         S (uax x) ≡ nat. 
 
 naxiom h : nat → nat.