models ported

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

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 1536476b09c0a91e22e9c3f87570dc58a6b54f7f..251352d1f6240f8a97275b7ffc3c9e6a4fe4597d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -23,63 +23,28 @@ lemma order_converges_bigger_lowsegment:
   ∀C:ordered_set.
    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. 
      ∀x:C.∀p:order_converge C a x. 
-       ∀j. seg_l (os_l C) s (λl.le (os_l C) l (pi1exT23 ???? p j)).
+       ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-cases (wloss_prop (os_l C))(W W);rewrite <W;
-[ intro H2; cases (SSa (seg_l_ C s) H2) (w Hw); simplify in Hw;
-  lapply (H (w+j)) as K; unfold in K;
-  whd in K:(? % ? ? ? ?); simplify in K:(%); rewrite <W in K; cases K;
-  whd in H1:(? % ? ? ? ?); simplify in H1:(%); rewrite <W in H1; 
-  simplify in H1; apply (H1 Hw);
-| intro H2; cases (SSa (seg_u_ C s) H2) (w Hw); simplify in Hw;
-  lapply (H (w+j)) as K; unfold in K;
-  whd in K:(? % ? ? ? ?);simplify in K:(%); rewrite <W in K; cases K; 
-  whd in H3:(? % ? ? ? ?);simplify in H3:(%); rewrite <W in H3;
-  simplify in H3; apply (H3 Hw);]
+intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
+lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
 qed.   
   
+alias symbol "upp" = "uppper".
+alias symbol "leq" = "Ordered set less or equal than".
 lemma order_converges_smaller_upsegment:
   ∀C:ordered_set.
    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. 
      ∀x:C.∀p:order_converge C a x. 
-       ∀j. seg_u (os_l C) s (λu.le (os_l C) (pi2exT23 ???? p j) u).
+       ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite <W;
-[ intro H2; cases (SIa (seg_u_ (os_l C) s) H2) (w Hw); simplify in Hw;
-  lapply (H (w+j)) as K; unfold in K; whd in K:(? % ? ? ? ?); simplify in K:(%); 
-  rewrite <W in K; cases K; whd in H3:(? % ? ? ? ?); simplify in H3:(%); rewrite <W in H3;
-  simplify in H3; apply (H3 Hw);
-| intro H2; cases (SIa (seg_l_ C s) H2) (w Hw); simplify in Hw;
-  lapply (H (w+j)) as K; unfold in K;  whd in K:(? % ? ? ? ?); simplify in K:(%);
-  rewrite <W in K; cases K; whd in H1:(? % ? ? ? ?); simplify in H1:(%);
-  rewrite <W in H1; simplify in H1; apply (H1 Hw);]
+intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K; 
+cases (cases_in_segment ? s ? K); apply H1; apply Hw;  
 qed. 
 
-lemma trans_under_upp:
- ∀O:ordered_set.∀s:‡O.∀x,y:O.
-  x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).
-intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
-apply (le_transitive ??? H H1);
-qed.
-
-lemma trans_under_low:
- ∀O:ordered_set.∀s:‡O.∀x,y:O.
-  y ≤ x → 𝕝_s (λl.l ≤ y) → 𝕝_s (λl.l ≤ x).
-intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
-apply (le_transitive ??? H1 H);
-qed.
-
-lemma l2sl:
-  ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
-intros; unfold in H ⊢ %; intro; apply H; clear H; unfold in H1 ⊢ %;
-cases (wloss_prop C) (W W); whd in H1:(? (% ? ?) ? ? ? ?); simplify in H1:(%); 
-rewrite < W in H1 ⊢ %; apply H1;
-qed.
-
 (* Theorem 3.10 *)
 theorem lebesgue_oc:
   ∀C:ordered_uniform_space.
@@ -95,12 +60,12 @@ generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 cut (∀i.xi i ∈ s) as Hxi; [2:
   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
+  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
+  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
 cut (∀i.yi i ∈ s) as Hyi; [2:
   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
+  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
 split;
 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
 |2: intros 3 (h);
@@ -136,12 +101,12 @@ generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 cut (∀i.xi i ∈ s) as Hxi; [2:
   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
+  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
+  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
 cut (∀i.yi i ∈ s) as Hyi; [2:
   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
+  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);