From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Jun 2008 11:23:59 +0000 (+0000)
Subject: lebesgue proved
X-Git-Tag: make_still_working~5045
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5070f476ff80ee53fe444d284f9e7587a37022f4;hp=c00f22f7afa508881c8d116928e1c460600ba0ac;p=helm.git

lebesgue proved
---

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 91a2335c7..21c10a4e1 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -25,11 +25,51 @@ inductive And (A,B:CProp) : CProp ≝
  
 interpretation "constructive and" 'and x y = (And x y).
 
+inductive And3 (A,B,C:CProp) : CProp ≝
+ | Conj3 : A → B → C → And3 A B C.
+
+notation < "a ∧ b ∧ c" left associative with precedence 60 for @{'and3 $a $b $c}.
+ 
+interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
+
+inductive And4 (A,B,C:CProp) : CProp ≝
+ | Conj4 : A → B → C → And4 A B C.
+
+notation < "a ∧ b ∧ c ∧ d" left associative with precedence 60 for @{'and3 $a $b $c $d}.
+ 
+interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
+
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
+inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
+  ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+
+notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
+notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
+notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
+notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
+notation < "'fst' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi12 $x $y}.
+notation < "'snd' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi22 $x $y}.
+
+definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
+
+interpretation "exT fst" 'pi1 x = (pi1exT _ _ x).
+interpretation "exT fst 2" 'pi12 x y = (pi1exT _ _ x y).
+
+definition pi1exT23 ≝
+  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
+definition pi2exT23 ≝
+  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
+   
+interpretation "exT2 fst" 'pi1 x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 snd" 'pi2 x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 fst 2" 'pi12 x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 snd 2" 'pi22 x y = (pi2exT23 _ _ _ _ x y).
+
+
 definition Not : CProp → Prop ≝ λx:CProp.x → False.
 
 interpretation "constructive not" 'not x = (Not x).
diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 1b34801d2..bab1e26fa 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -16,20 +16,30 @@
 include "sandwich.ma".
 include "property_exhaustivity.ma".
 
-lemma foo:
+lemma order_converges_bigger_lowsegment:
   ∀C:ordered_set.
    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.∀p:a order_converges x. 
-       ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j).
-intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
-cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
-cases H2; clear H2;  intro; cases (H5 ? H2);
-cases (H (w2+j)); apply (H8 H6);
+       ∀j.l ≤ (fst p) j.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H8 ? H2);
+cases (H (w1+j)); apply (H12 H7);
+qed.   
+
+lemma order_converges_smaller_upsegment:
+  ∀C:ordered_set.
+   ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.∀p:a order_converges x. 
+       ∀j.(snd p) j ≤ u.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H10 ? H2);
+cases (H (w1+j)); apply (H11 H7);
 qed.   
-     
      
 (* Theorem 3.10 *)
-theorem lebesgue:
+theorem lebesgue_oc:
   ∀C:ordered_uniform_space.
    (∀l,u:C.order_continuity {[l,u]}) →
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
@@ -41,15 +51,41 @@ theorem lebesgue:
          (segment_ordered_uniform_space C l u))
         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
         (sig_in ?? x h).
-intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; 
-cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
+intros;
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+  intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+  apply (le_transitive ???? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+  intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+  apply (le_transitive ????? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H2;
 split;
-[2: intro h;
-  cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
-
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+    [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+    |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3 (h);
+    letin X ≝ (sig_in ?? x h);
+    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+        [apply (H5 0);|apply (H7 0)]
+    |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        exists [apply w] apply H7; 
+    |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        exists [apply w] apply H7;]]
+qed.
+ 
 
 (* Theorem 3.9 *)
-theorem lebesgue:
+theorem lebesgue_se:
   ∀C:ordered_uniform_space.property_sigma C →
    (∀l,u:C.exhaustive {[l,u]}) →
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
@@ -61,22 +97,34 @@ theorem lebesgue:
          (segment_ordered_uniform_space C l u))
         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
         (sig_in ?? x h). 
-intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8; 
-cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
-lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
-lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
-cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x); 
-[ split; assumption]
-split; simplify;
- [1: intro;  cases (H7 n); cases H3;
- 
- 
- lapply (sandwich ? x xi yi a );
-  [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
-  |3: intros 2;  
-      cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x); 
-      [1: 
-
-lapply (restrict_uniform_convergence ? H ?? (H1 l u) 
-         (λn:nat.sig_in ?? (a n) (H2 n)) x);
-  [2:split; assumption]
\ No newline at end of file
+intros (C S);
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+  intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+  apply (le_transitive ???? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+  intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+  apply (le_transitive ????? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H2;
+split;
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+    [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+    |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3;
+    lapply (uparrow_upperlocated ? xi x Hx)as Ux;
+    lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
+    letin X ≝ (sig_in ?? x h);
+    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+        [apply (H5 0);|apply (H7 0)]
+    |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
+        apply (H4 h);
+    |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
+        apply (H4 h);]]
+qed. 
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index b9bb51e3b..cf3a5b057 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -39,6 +39,14 @@ intros; cases H (Ha Hx); split [apply Ha] cases Hx;
 split; [apply H1] intros;
 cases (H2 (fst y) H3); exists [apply w] assumption;
 qed.
+
+lemma segment_preserves_downarrow:
+  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
+    (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h).
+intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
+split; [apply H1] intros;
+cases (H2 (fst y) H3); exists [apply w] assumption;
+qed.
     
 (* Fact 2.18 *)
 lemma segment_cauchy:
@@ -53,7 +61,7 @@ intro; cases b; intros; simplify; split; intros; assumption;
 qed.       
 
 (* Lemma 3.8 *)
-lemma restrict_uniform_convergence:
+lemma restrict_uniform_convergence_uparrow:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀l,u:C.exhaustive {[l,u]} →
      ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↑ x → 
@@ -71,7 +79,28 @@ intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
       [2:split; assumption]; cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H6 H4 Ha1) as HaC;
     lapply (segment_cauchy ? l u ? HaC) as Ha;
-    lapply (sigma_cauchy ? H  ? x ? Ha); [split; assumption]
+    lapply (sigma_cauchy ? H  ? x ? Ha); [left; split; assumption]
     apply restric_uniform_convergence; assumption;]
 qed.
-       
\ No newline at end of file
+      
+lemma restrict_uniform_convergence_downarrow:
+  ∀C:ordered_uniform_space.property_sigma C →
+    ∀l,u:C.exhaustive {[l,u]} →
+     ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↓ x → 
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h).
+intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
+[1: split;
+    [2: apply (infimum_is_lower_bound C ?? Hx l); 
+        apply (segment_lowerbound ? l u);
+    |1: apply (le_transitive ?? (fst (a 0))); [apply H2;]
+        apply (segment_upperbound ? l u);]
+|2: intros;
+    lapply (downarrow_lowerlocated ? a (sig_in ?? x h)) as Ha1;
+      [2: apply segment_preserves_downarrow;split; assumption;] 
+    lapply (segment_preserves_infimum ?l u a (sig_in ??? h)) as Ha2; 
+      [2:split; assumption]; cases Ha2; clear Ha2;
+    cases (H1 a a); lapply (H7 H4 Ha1) as HaC;
+    lapply (segment_cauchy ? l u ? HaC) as Ha;
+    lapply (sigma_cauchy ? H  ? x ? Ha); [right; split; assumption]
+    apply restric_uniform_convergence; assumption;]
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index f6a315c82..757c18a07 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -22,7 +22,7 @@ definition property_sigma ≝
    ∀U.us_unifbase ? U → 
      ∃V:sequence (C square → Prop).
        (∀i.us_unifbase ? (V i)) ∧ 
-       ∀a:sequence C.∀x:C.a ↑ x → 
+       ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) → 
          (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
       
 definition max ≝
@@ -58,7 +58,6 @@ 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.
 
-
 definition hide ≝ λT:Type.λx:T.x.
 
 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
@@ -73,9 +72,8 @@ coercion cic:/matita/dama/property_sigma/eject.con.
 (* Lemma 3.6 *)   
 lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
-    ∀a:sequence C.∀l:C.a ↑ l → a is_cauchy → a uniform_converges l.
-intros 8; cases H1; cases H5; clear H5;
-cases (H ? H3); cases H5; clear H5;
+    ∀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;
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with
   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
@@ -86,15 +84,15 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   [1,2:apply H8;
   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
       simplify in ⊢ (?→? (? % ?) ?→?);
-      intros; lapply (H10 i j) as H14;
-        [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);]
-      cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption]
-      generalize in match H11; generalize in match H12;
+      intros; lapply (H5 i j) as H14;
+        [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
+      cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
+      generalize in match H6; generalize in match H7;
       cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
-      apply H16; [3: apply le_S_S_to_le; assumption]
+      apply H12; [3: apply le_S_S_to_le; assumption]
       apply lt_to_le; apply (max_le_r w1); assumption;
-  |4: intros; clear H11; rewrite > H5 in H10; 
-      rewrite < (le_n_O_to_eq ? H14); apply H10; 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:
   intro n; change with (S (m n) ≤ m (S n)); unfold m; 
   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
@@ -103,24 +101,28 @@ cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
   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;
-lapply (selection ?? Hm a l H1) as H10; 
+cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.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);]] 
 lapply (H9 ?? H10) as H11; [
   exists [apply (m 0:nat)] intros;
-  apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
-  simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
-  change with (a (m O) ≤ a i);
-  apply (trans_increasing ?? H4); intro; whd in H12;
-  apply (not_le_Sn_n i);  apply (transitive_le ??? H12 H5)]
+  cases H1;
+    [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
+    |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉); 
+     lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
+  simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
+  [1:change with (a (m O) ≤ a i);
+     apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
+  |2:change with (a i ≤ a (m O));
+     apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]  
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
 generalize in match (refl_eq nat (m p)); 
-(*
-intro E; cases p in E : (? ? ? ?);
-*)
 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
 intros (H16); simplify in H16:(? ? ? %); destruct H16;
 apply H15; [3: apply le_n]
 [1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p q H5);
+    apply (le_to_not_lt p q H4);
 |2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p r H10);]
+    apply (le_to_not_lt p r H5);]
 qed.
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 50b1ebeda..1e6c95b8d 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -79,6 +79,14 @@ intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
 cases (H1 ? H) (w Hw); apply Hv; assumption;
 qed.
 
+lemma infimum_is_lower_bound: 
+  ∀C:ordered_set.∀a:sequence C.∀u:C.
+   u is_infimum a → ∀v.v is_lower_bound a → v ≤ u.
+intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
+cases (H1 ? H) (w Hw); apply Hv; assumption;
+qed.
+
+
 (* Lemma 2.6 *)
 definition strictly_increasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
@@ -98,17 +106,22 @@ notation > "s 'is_strictly_decreasing'" non associative with precedence 50
   for @{'strictly_decreasing $s}.
 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
   (strictly_decreasing _ s).
-  
-notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
-interpretation "Ordered set supremum of increasing" 'sup_inc s u =
- (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) 
-  (increasing _ s)
-  (supremum _ s u)).
-notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
-interpretation "Ordered set supremum of increasing" 'inf_dec s u =
- (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) 
-  (decreasing _ s)
-  (infimum _ s u)).
+
+definition uparrow ≝
+  λC:ordered_set.λs:sequence C.λu:C.
+   s is_increasing ∧ u is_supremum s.
+   
+definition downarrow ≝
+  λC:ordered_set.λs:sequence C.λu:C.
+   s is_decreasing ∧ u is_infimum s.
+     
+notation < "a \uparrow \nbsp u" non associative with precedence 50 for @{'sup_inc $a $u}.
+notation > "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
+interpretation "Ordered set uparrow" 'sup_inc s u = (uparrow _ s u).
+
+notation < "a \downarrow \nbsp u" non associative with precedence 50 for @{'inf_dec $a $u}.
+notation > "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
+interpretation "Ordered set downarrow" 'inf_dec s u = (downarrow _ s u).
 
 include "nat/plus.ma".
 include "nat_ordered_set.ma".
@@ -126,6 +139,17 @@ cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
     intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
 qed.
 
+lemma trans_decreasing: 
+  ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
+intros 5 (C a Hs n m); elim m; [
+  rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
+  intro X; cases (os_coreflexive ?? X);]
+cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
+[2: rewrite > H2; intro; cases (os_coreflexive ?? H1);
+|1: apply (le_transitive ???? (Hs ?) (H ?));
+    intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
+qed.
+
 lemma trans_increasing_exc: 
   ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
@@ -138,6 +162,18 @@ intro; apply H;
     cases (Hs n1); assumption;]
 qed.
 
+lemma trans_decreasing_exc: 
+  ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n .
+intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
+intro; apply H; 
+[1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) 
+    change with (n<n1); (* is sort elimination not allowed preserved by delta? *)
+    cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
+    cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)    
+|2: cases (os_cotransitive ??? (a n1) H2); [2:assumption]
+    cases (Hs n1); assumption;]
+qed.
+
 lemma strictly_increasing_reaches: 
   ∀C:ordered_set.∀m:sequence nat_ordered_set.
    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
@@ -154,7 +190,7 @@ intros; elim w;
         apply (transitive_le ??? H2 Hp);]]
 qed.
      
-lemma selection: 
+lemma selection_uparrow: 
   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
     ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
@@ -165,15 +201,25 @@ intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]  
     cases (trans_increasing_exc C ? Ia ?? H1); assumption;]
 qed.     
-    
+
+lemma selection_downarrow: 
+  ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
+    ∀a:sequence C.∀u.a ↓ u → (λx.a (m x)) ↓ u.
+intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
+[1: intro n; simplify; apply trans_decreasing_exc; [assumption] apply (Hm n);
+|2: intro n; simplify; apply Uu;
+|3: intros (y Hy); simplify; cases (Hu ? Hy);
+    cases (strictly_increasing_reaches C ? Hm w); 
+    exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [assumption]  
+    cases (trans_decreasing_exc C ? Ia ?? H1); assumption;]
+qed.     
+
 (* Definition 2.7 *)
-alias symbol "exists" = "CProp exists".
-alias symbol "and" = "constructive and".
+alias id "ExT23" = "cic:/matita/dama/cprop_connectives/exT23.ind#xpointer(1/1)".
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
-   ∃l:sequence O.∃u:sequence O.
-    (*l is_increasing ∧ u is_decreasing ∧*) l ↑ x ∧ u ↓ x ∧
-    ∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i)).
+   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))).
     
 notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
   for @{'order_converge $a $x}.
@@ -198,10 +244,6 @@ coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A
 
 definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
 
-notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
-notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
-notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
 interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x).
  
 interpretation "Type exists" 'exists \eta.x =
@@ -232,6 +274,18 @@ intros; split; cases H; clear H;
     |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.
+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));]]
+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].
@@ -312,5 +366,3 @@ cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
 [1: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
 |2: right; exists [apply u]; split; [apply W|apply H4]]
 qed. 
-     
-