1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* manca un pezzo del pullback, se inverto poi non tipa *)
16 include "sandwich.ma".
17 include "property_exhaustivity.ma".
20 alias symbol "low" = "lower".
21 alias id "le" = "cic:/matita/dama/ordered_set/le.con".
22 lemma order_converges_bigger_lowsegment:
24 ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
25 ∀x:C.∀p:order_converge C a x.
26 ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
27 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
28 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
29 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
30 intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
31 lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
34 alias symbol "upp" = "uppper".
35 alias symbol "leq" = "Ordered set less or equal than".
36 lemma order_converges_smaller_upsegment:
38 ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
39 ∀x:C.∀p:order_converge C a x.
40 ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
41 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
42 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
43 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
44 intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K;
45 cases (cases_in_segment ? s ? K); apply H1; apply Hw;
50 ∀C:ordered_uniform_space.
51 (∀s:‡C.order_continuity {[s]}) →
52 ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
53 ∀x:C.a order_converges x →
56 uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
58 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
59 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
60 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
61 cut (∀i.xi i ∈ s) as Hxi; [2:
62 intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
63 lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
64 simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
65 cut (∀i.yi i ∈ s) as Hyi; [2:
66 intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
67 lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
68 apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
70 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
72 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
73 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
74 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
75 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
76 [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
77 [apply (l2sl ? s (Xi j) (Ai j) (H5 0));|apply (l2sl ? s (Ai j) (Yi j) (H7 0))]
78 |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl ? s (Xi i) (Xi (S i)) (H3 i));]
79 cases H4; split; [intro i; apply (l2sl ? s (Xi i) ≪x,h≫ (H5 i))]
80 intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s ? y Hy)]
81 exists [apply w] apply (x2sx ? s (Xi w) y H7);
82 |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl ? s (Yi (S i)) (Yi i) (H3 i));]
83 cases H4; split; [intro i; apply (l2sl ? s ≪x,h≫ (Yi i) (H5 i))]
84 intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s y ≪x,h≫ Hy)]
85 exists [apply w] apply (x2sx ? s y (Yi w) H7);]]
91 ∀C:ordered_uniform_space.property_sigma C →
92 (∀s:‡C.exhaustive {[s]}) →
93 ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
94 ∀x:C.a order_converges x →
97 uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
99 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
100 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
101 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
102 cut (∀i.xi i ∈ s) as Hxi; [2:
103 intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
104 lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
105 simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
106 cut (∀i.yi i ∈ s) as Hyi; [2:
107 intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
108 lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
109 apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
110 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
111 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
112 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
113 cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
114 split; [1: assumption]
116 lapply (uparrow_upperlocated xi x Hx)as Ux;
117 lapply (downarrow_lowerlocated yi x Hy)as Uy;
118 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
119 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
120 intro j; cases (Hxy j); cases H7; cases H8; split;
121 [apply (l2sl ? s (Xi j) (Ai j) (H9 0));|apply (l2sl ? s (Ai j) (Yi j) (H11 0))]