models over N fixed

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

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index f53cdc45814862a707493c7b3409a84bf7d75377..b4430d6edff7d4daaa16eaa9a899786a4dea2498 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -217,7 +217,7 @@ qed.
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
+     (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
@@ -227,7 +227,6 @@ notation > "a 'order_converges' x" non associative with precedence 45
 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
     
 (* Definition 2.8 *)
-alias symbol "and" = "constructive and".
 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
 notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
@@ -239,8 +238,8 @@ interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
-intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
-[1: intros (x y); apply (fst x ≰ fst y);
+intros (O u v); apply (mk_ordered_set (sigT ? (λx.x ∈ [u,v])));
+[1: intros (x y); apply (\fst x ≰ \fst y);
 |2: intro x; cases x; simplify; apply os_coreflexive;
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
 qed.
@@ -253,24 +252,24 @@ interpretation "Ordered set segment" 'segment_set a b =
 (* Lemma 2.9 *)
 lemma segment_preserves_supremum:
   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
-    ⌊n,fst (a n)⌋ is_increasing ∧ 
-    (fst x) is_supremum ⌊n,fst (a n)⌋ → a ↑ x.
+    ⌊n,\fst (a n)⌋ is_increasing ∧ 
+    (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x.
 intros; split; cases H; clear H; 
 [1: apply H1;
 |2: cases H2; split; clear H2;
     [1: apply H;
-    |2: clear H; intro y0; apply (H3 (fst y0));]]
+    |2: clear H; intro y0; apply (H3 (\fst y0));]]
 qed.
 
 lemma segment_preserves_infimum:
   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
-    ⌊n,fst (a n)⌋ is_decreasing ∧ 
-    (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x.
+    ⌊n,\fst (a n)⌋ is_decreasing ∧ 
+    (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
 intros; split; cases H; clear H; 
 [1: apply H1;
 |2: cases H2; split; clear H2;
     [1: apply H;
-    |2: clear H; intro y0; apply (H3 (fst y0));]]
+    |2: clear H; intro y0; apply (H3 (\fst y0));]]
 qed.
 
 (* Definition 2.10 *)
@@ -279,11 +278,11 @@ alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
 definition square_segment ≝ 
   λO:ordered_set.λa,b:O.λx:O square.
-    And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
+    And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
  
 definition convex ≝
   λO:ordered_set.λU:O square → Prop.
-    ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
+    ∀p.U p → \fst p ≤ \snd p → ∀y. square_segment ? (\fst p) (\snd p) y → U y.
   
 (* Definition 2.11 *)  
 definition upper_located ≝