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".
19 alias num (instance 0) = "natural number".
20 definition property_sigma ≝
21 λC:ordered_uniform_space.
23 ∃V:sequence (C square → Prop).
24 (∀i.us_unifbase ? (V i)) ∧
25 ∀a:sequence C.∀x:C.a ↑ x →
26 (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
29 λm,n.match leb n m with [true ⇒ m | false ⇒ n].
31 lemma le_max: ∀n,m.m ≤ max n m.
32 intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
35 definition hide ≝ λT:Type.λx:T.x.
37 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
38 interpretation "hide" 'hide =
39 (cic:/matita/dama/property_sigma/hide.con _ _).
43 ∀O:ordered_uniform_space.property_sigma O →
44 ∀a:sequence O.∀l:O.a ↑ l → a is_cauchy → a uniform_converges l.
45 intros 8; cases H1; cases H5; clear H5;
46 cases (H ? H3); cases H5; clear H5;
47 letin m ≝ (? : sequence nat_ordered_set); [
48 apply (hide (nat→nat)); intro i; elim i (i' Rec);
49 [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k;
50 |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]]
51 cut (m is_strictly_increasing) as Hm; [2:
52 intro n; change with (S (m n) ≤ m (S n)); unfold m; whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
53 lapply (selection ?? Hm a l H1) as H10;
54 lapply (H9 ?? H10) as H11;
55 [1: exists [apply (m 0)] intros;
56 apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
57 simplify; repeat split;