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 (**************************************************************************)
17 record ordered_uniform_space_ : Type ≝ {
19 ous_us_: uniform_space;
20 with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os
23 lemma ous_unifspace: ordered_uniform_space_ → uniform_space.
24 intro X; apply (mk_uniform_space (bishop_set_of_ordered_set X));
25 unfold bishop_set_OF_ordered_uniform_space_;
26 [1: rewrite < (with_ X); simplify; apply (us_unifbase (ous_us_ X));
27 |2: cases (with_ X); simplify; apply (us_phi1 (ous_us_ X));
28 |3: cases (with_ X); simplify; apply (us_phi2 (ous_us_ X));
29 |4: cases (with_ X); simplify; apply (us_phi3 (ous_us_ X));
30 |5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))]
33 coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con.
35 record ordered_uniform_space : Type ≝ {
36 ous_stuff :> ordered_uniform_space_;
37 ous_prop1: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
41 lemma segment_ordered_uniform_space:
42 ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
43 intros (O u v); apply mk_ordered_uniform_space;
44 [1: apply mk_ordered_uniform_space_;
45 [1: apply (mk_ordered_set (sigma ? (λx.x ∈ [u,v])));
46 [1: intros (x y); apply (fst x ≰ fst y);
47 |2: intros 1; cases x; simplify; apply os_coreflexive;
48 |3: intros 3; cases x; cases y; cases z; simplify; apply os_cotransitive]
49 |2: apply (mk_uniform_space (bishop_set_of_ordered_set (mk_ordered_set (sigma ? (λx.x ∈ [u,v])) ???)));
56 ∀O:ordered_uniform_space.∀l,u:O.
57 ∀x:(segment_ordered_uniform_space O l u).
58 ∀a:sequence (segment_ordered_uniform_space O l u).
59 (* (λn.fst (a n)) uniform_converges (fst x) → *)
60 a uniform_converges x.