some notation added with a bit PITA

[helm.git] / helm / software / matita / contribs / dama / dama / property_sigma.ma

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index ece02e9ba982f11bfbb8688428cb6e28a8ce9fed..ba90bb0ab50097e864bdf9c884902aa049098c44 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -57,19 +57,20 @@ qed.
 lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
 intros; rewrite > sym_max in H; apply (max_le_l ??? H); 
 qed.
-      
+    
 (* Lemma 3.6 *)   
 lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
+alias symbol "pair" = "pair".
+letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with
   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
   | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
   ] in aux
-  : 
-  ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+  : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
   [1,2:apply H8;
   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
       simplify in ⊢ (?→? (? % ?) ?→?);
@@ -82,15 +83,15 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
       apply lt_to_le; apply (max_le_r w1); assumption;
   |4: intros; clear H6; rewrite > H4 in H5; 
       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
-cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
   intro n; change with (S (m n) ≤ m (S n)); unfold m; 
   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
   intro n; intro L; change in L with (m (S n) < m n);
   lapply (Hm n) as L1; change in L1 with (m n < m (S n));
   lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] 
-clearbody m;
-cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2: 
+clearbody m; unfold spec in m Hm Hm1; clear spec;
+cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: 
  cases H1;
  [ left; apply (selection_uparrow ?? Hm a l H4);
  | right; apply (selection_downarrow ?? Hm a l H4);]]