...

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 7bb312aff0284a0a6bef069af9d5fe19e4115a18..5cf875f80a1455fb3cc4aebac6838a3d5e195b83 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -17,15 +17,15 @@ include "supremum.ma".
 include "nat/le_arith.ma".
 include "russell_support.ma".
 
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); 
+intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
 fold normalize X; intros; cases H1; 
 alias symbol "plus" = "natural plus".
-alias symbol "nat" = "Uniform space N".
+alias symbol "N" = "Uniform space N".
 alias symbol "and" = "logical and".
 letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); 
 (* s - aj <= max 0 (u - i) *)  
@@ -114,9 +114,9 @@ apply le_to_le_to_eq;
     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 qed.
 
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
-alias symbol "nat" = "ordered set N".
+alias symbol "N" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).