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".
19 le x_i e y_i stanno o no nel segmento?
23 ∀C:ordered_uniform_space.
24 (∀l,u:C.order_continuity {[l,u]}) →
25 ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
26 ∀x:C.a order_converges x →
28 ∀h:x ∈ [l,u]. (* manca il pullback? *)
30 (uniform_space_OF_ordered_uniform_space
31 (segment_ordered_uniform_space C l u))
32 (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
34 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5;
35 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
37 [2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h));
42 ∀C:ordered_uniform_space.property_sigma C →
43 (∀l,u:C.exhaustive {[l,u]}) →
44 ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
45 ∀x:C.a order_converges x →
47 ∀h:x ∈ [l,u]. (* manca il pullback? *)
49 (uniform_space_OF_ordered_uniform_space
50 (segment_ordered_uniform_space C l u))
51 (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
53 intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8;
54 cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
55 lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
56 lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
57 cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x);
60 [1: intro; cases (H7 n); cases H3;
63 lapply (sandwich ? x xi yi a );
64 [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
66 cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x);
69 lapply (restrict_uniform_convergence ? H ?? (H1 l u)
70 (λn:nat.sig_in ?? (a n) (H2 n)) x);