update in groud_2 and models

[helm.git] / helm / software / matita / nlibrary / topology / cantor.ma

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index fd300462e918aeecc8add2b9b358a81614a278cf..6a79dd2d808df2478f6a4ad25568e41e1eb68894 100644 (file)
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -41,7 +41,7 @@ ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
 ##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); /2/;
+##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); /3/;
 ##] 
 nqed.
 
@@ -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.