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 include "ordered_uniform.ma".
16 include "property_sigma.ma".
19 definition exhaustive ≝
20 λC:ordered_uniform_space.
22 (a is_increasing → a is_upper_located → a is_cauchy) ∧
23 (b is_decreasing → b is_lower_located → b is_cauchy).
25 lemma h_segment_upperbound:
28 ∀a:sequence (half_segment_ordered_set C s).
29 (seg_u C s) (upper_bound ? ⌊n,\fst (a n)⌋).
30 intros; cases (wloss_prop C); unfold; rewrite < H; simplify; intro n;
31 cases (a n); simplify; unfold in H1; rewrite < H in H1; cases H1;
32 simplify in H2 H3; rewrite < H in H2 H3; assumption;
35 notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
36 notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
38 interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
39 interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
41 lemma h_segment_preserves_uparrow:
42 ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
43 ∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
44 intros; cases H (Ha Hx); split;
45 [ intro n; intro H; apply (Ha n); apply (sx2x ???? H);
47 [ intro n; intro H; apply (H1 n);apply (sx2x ???? H);
48 | intros; cases (H2 (\fst y)); [2: apply (sx2x ???? H3);]
49 exists [apply w] apply (x2sx ?? (a w) y H4);]]
52 notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
53 notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
55 interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
56 interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
63 (ordered_set_OF_ordered_uniform_space C) s))
65 sequence (Type_OF_uniform_space (segment_ordered_uniform_space C s)). intros; assumption;
68 coercion hint_pippo nocomposites.
72 ∀C:ordered_uniform_space.∀s:‡C.∀a:sequence {[s]}.
73 a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy.
75 alias symbol "pi1" (instance 3) = "pair pi1".
76 alias symbol "pi2" = "pair pi2".
77 apply (H (λx:{[s]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
78 (unfold segment_ordered_uniform_space; simplify);
79 exists [apply U] split; [assumption;]
80 intro; cases b; intros; simplify; split; intros; assumption;
83 (* Lemma 3.8 NON DUALIZZATO *)
84 lemma restrict_uniform_convergence_uparrow:
85 ∀C:ordered_uniform_space.property_sigma C →
86 ∀l,u:C.exhaustive {[l,u]} →
87 ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↑ x →
88 x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
89 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
91 [1: apply (supremum_is_upper_bound ? x Hx u);
92 apply (segment_upperbound ? l);
93 |2: apply (le_transitive l ? x ? (H2 O));
94 apply (segment_lowerbound ? l u a 0);]
96 lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
97 [2: apply (segment_preserves_uparrow C l u);split; assumption;]
98 lapply (segment_preserves_supremum C l u a ≪?,h≫) as Ha2;
99 [2:split; assumption]; cases Ha2; clear Ha2;
100 cases (H1 a a); lapply (H6 H4 Ha1) as HaC;
101 lapply (segment_cauchy ? l u ? HaC) as Ha;
102 lapply (sigma_cauchy ? H ? x ? Ha); [left; split; assumption]
103 apply restric_uniform_convergence; assumption;]
107 ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
108 intros; assumption; qed.
110 coercion hint_mah1 nocomposites.
113 ∀C. sequence (hos_carr (os_l C)) → sequence (hos_carr (os_r C)).
114 intros; assumption; qed.
116 coercion hint_mah2 nocomposites.
119 ∀C. Type_OF_ordered_uniform_space C → hos_carr (os_r C).
120 intros; assumption; qed.
122 coercion hint_mah3 nocomposites.
125 ∀C. sequence (hos_carr (os_r C)) → sequence (hos_carr (os_l C)).
126 intros; assumption; qed.
128 coercion hint_mah4 nocomposites.
130 lemma restrict_uniform_convergence_downarrow:
131 ∀C:ordered_uniform_space.property_sigma C →
132 ∀l,u:C.exhaustive {[l,u]} →
133 ∀a:sequence {[l,u]}.∀x: C. ⌊n,\fst (a n)⌋ ↓ x →
134 x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
135 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
137 [2: apply (infimum_is_lower_bound ? x Hx l);
138 apply (segment_lowerbound ? l u);
139 |1: lapply (ge_transitive ? ? x ? (H2 O)); [apply u||assumption]
140 apply (segment_upperbound ? l u a 0);]
142 lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1;
143 [2: apply (segment_preserves_downarrow ? l u);split; assumption;]
144 lapply (segment_preserves_infimum C l u a ≪x,h≫) as Ha2;
145 [2:split; assumption]; cases Ha2; clear Ha2;
146 cases (H1 a a); lapply (H7 H4 Ha1) as HaC;
147 lapply (segment_cauchy ? l u ? HaC) as Ha;
148 lapply (sigma_cauchy ? H ? x ? Ha); [right; split; assumption]
149 apply restric_uniform_convergence; assumption;]