X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=6d5879a8378e6fcd92c71dfeeba7785af5942580;hb=7e33e23e18dc5d008b3b3dc0052aa4d7b236415e;hp=ea5c550507a941b778096cda1059f74eb472159a;hpb=3c1ca5620048ad842144fba291f8bc5f0dca7061;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index ea5c55050..6d5879a83 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -216,7 +216,7 @@ qed.
 (* Definition 2.7 *)
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
-   ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
+   exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
      (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
@@ -237,16 +237,6 @@ notation "hvbox(x \in break [a,b])" non associative with precedence 45
   for @{'segment_in $a $b $x}.
 interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
-(*
-coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
-
-definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
-
-interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x).
- 
-interpretation "Type exists" 'exists \eta.x = (sigma _ 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]));
@@ -284,41 +274,11 @@ intros; split; cases H; clear H;
 qed.
 
 (* Definition 2.10 *)
-coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. 
-definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
-definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (prod _ _ a b).
-interpretation "prod" 'product a b = (pair a b).
-
-lemma square_ordered_set: ordered_set → ordered_set.
-intro O;
-apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
-|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
-    cases H (X X); apply (os_coreflexive ?? X);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
-    clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
-    [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
-    |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
-qed.
-
-notation < "s 2 \atop \nleq" non associative with precedence 90
-  for @{ 'square $s }.
-notation > "s 'square'" non associative with precedence 90
-  for @{ 'square $s }.
-interpretation "ordered set square" 'square s = (square_ordered_set s).
- 
+alias symbol "square" = "ordered set square".
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
 definition square_segment ≝ 
-  λO:ordered_set.λa,b:O.λx:square_ordered_set O.
+  λO:ordered_set.λa,b:O.λx:O square.
     And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
  
 definition convex ≝