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".
21 ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
22 ∀x:C.∀p:a order_converges x.
23 ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j).
24 intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
25 cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
26 cases H2; clear H2; intro; cases (H5 ? H2);
27 cases (H (w2+j)); apply (H8 H6);
33 ∀C:ordered_uniform_space.
34 (∀l,u:C.order_continuity {[l,u]}) →
35 ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
36 ∀x:C.a order_converges x →
38 ∀h:x ∈ [l,u]. (* manca il pullback? *)
40 (uniform_space_OF_ordered_uniform_space
41 (segment_ordered_uniform_space C l u))
42 (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
44 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5;
45 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
48 cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h));
53 ∀C:ordered_uniform_space.property_sigma C →
54 (∀l,u:C.exhaustive {[l,u]}) →
55 ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
56 ∀x:C.a order_converges x →
58 ∀h:x ∈ [l,u]. (* manca il pullback? *)
60 (uniform_space_OF_ordered_uniform_space
61 (segment_ordered_uniform_space C l u))
62 (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
64 intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8;
65 cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
66 lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
67 lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
68 cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x);
71 [1: intro; cases (H7 n); cases H3;
74 lapply (sandwich ? x xi yi a );
75 [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
77 cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x);
80 lapply (restrict_uniform_convergence ? H ?? (H1 l u)
81 (λn:nat.sig_in ?? (a n) (H2 n)) x);