helm/software/matita/contribs/dama/dama/ordered_uniform.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "uniform.ma".
  16
  17 record ordered_uniform_space_ : Type ≝ {
  18   ous_os:> ordered_set;
  19   ous_us_: uniform_space;
  20   with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os
  21 }.
  22
  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))]
  31 qed.
  32
  33 coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con.
  34
  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
  38 }.
  39
  40
  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])) ???)));
  50     |3: apply refl_eq;
  51 qed.
  52
  53
  54 (* Lemma 3.2 *)
  55 lemma foo:
  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.
  61
  62