helm/software/matita/contribs/dama/dama/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 "supremum.ma".
  16
  17 (* Definition 2.13 *)
  18 definition square_bishop_set : bishop_set → bishop_set.
  19 intro S; apply (mk_bishop_set (pair S S));
  20 [1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
  21 |2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
  22 |3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
  23 |4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
  24     [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
  25     |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
  26 qed.
  27
  28 definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
  29
  30 notation "a \subseteq u" left associative with precedence 70
  31   for @{ 'subset $a $u }.
  32 interpretation "Bishop subset" 'subset a b =
  33   (cic:/matita/dama/uniform/subset.con _ a b).
  34
  35 notation "{ ident x : t | p }" non associative with precedence 50
  36   for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.
  37 definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
  38 interpretation "explicit set" 'explicitset t =
  39   (cic:/matita/dama/uniform/mk_set.con _ t).
  40
  41 notation < "s \sup 2" non associative with precedence 90
  42   for @{ 'square $s }.
  43 notation > "s 'square'" non associative with precedence 90
  44   for @{ 'square $s }.
  45 interpretation "bishop suqare set" 'square x =
  46   (cic:/matita/dama/uniform/square_bishop_set.con x).
  47
  48 alias symbol "exists" = "exists".
  49 alias symbol "and" = "logical and".
  50 definition compose_relations ≝
  51   λC:bishop_set.λU,V:C square → Prop.
  52    λx:C square.∃y:C. U (prod ?? (fst x) y) ∧ V (prod ?? y (snd x)).
  53
  54 notation "a \circ b"  left associative with precedence 60
  55   for @{'compose $a $b}.
  56 interpretation "relations composition" 'compose a b =
  57  (cic:/matita/dama/uniform/compose_relations.con _ a b).
  58
  59 definition invert_relation ≝
  60   λC:bishop_set.λU:C square → Prop.
  61     λx:C square. U (prod ?? (snd x) (fst x)).
  62
  63 notation < "s \sup (-1)"  non associative with precedence 90
  64   for @{ 'invert $s }.
  65 notation > "'inv' s" non associative with precedence 90
  66   for @{ 'invert $s }.
  67 interpretation "relation invertion" 'invert a =
  68  (cic:/matita/dama/uniform/invert_relation.con _ a).
  69
  70 record uniform_space : Type ≝ {
  71   us_carr:> bishop_set;
  72   us_unifbase: (us_carr square → Prop) → CProp;
  73   us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
  74     {x:us_carr square|fst x ≈ snd x} ⊆ U;
  75   us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
  76     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
  77   us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
  78     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
  79   us_phi4: ∀U:us_carr square → Prop. us_unifbase U → U = inv U (* I should use double inclusion ... *)
  80 }.
  81
  82 (* Definition 2.14 *)
  83 alias symbol "leq" = "natural 'less or equal to'".
  84 definition cauchy ≝
  85   λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
  86    ∃n. ∀i,j. n ≤ i → n ≤ j → U (prod ?? (a i) (a j)).
  87
  88 notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
  89   for @{'cauchy $a}.
  90 notation > "a 'is_cauchy'" non associative with precedence 50
  91   for @{'cauchy $a}.
  92 interpretation "Cauchy sequence" 'cauchy s =
  93  (cic:/matita/dama/uniform/cauchy.con _ s).
  94
  95 (* Definition 2.15 *)
  96 definition uniform_converge ≝
  97   λC:uniform_space.λa:sequence C.λu:C.
  98     ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U (prod ?? u (a i)).
  99
 100 notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
 101   for @{'uniform_converge $a $x}.
 102 notation > "a 'uniform_converges' x" non associative with precedence 50
 103   for @{'uniform_converge $a $x}.
 104 interpretation "Uniform convergence" 'uniform_converge s u =
 105  (cic:/matita/dama/uniform/uniform_converge.con _ s u).
 106
 107 (* Lemma 2.16 *)
 108 lemma uniform_converge_is_cauchy :
 109   ∀C:uniform_space.∀a:sequence C.∀x:C.
 110    a uniform_converges x → a is_cauchy.
 111 intros (C a x Ha); intros 2 (u Hu);
 112 cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
 113 cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
 114 apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
 115 rewrite > (us_phi4 ?? Hv); simplify; apply (Hn ? H1);
 116 qed.
 117
 118 (* Definition 2.17 *)
 119 definition mk_big_set ≝
 120   λP:CProp.λF:P→CProp.F.
 121 interpretation "explicit big set" 'explicitset t =
 122   (cic:/matita/dama/uniform/mk_big_set.con _ t).
 123
 124 definition restrict_uniformity ≝
 125   λC:uniform_space.λX:C→Prop.
 126    {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.
 127
 128