helm/software/matita/library/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 "dama/supremum.ma".
  16
  17 (* Definition 2.13 *)
  18 alias symbol "pair" = "Pair construction".
  19 alias symbol "exists" = "exists".
  20 alias symbol "and" = "logical and".
  21 definition compose_bs_relations ≝
  22   λC:bishop_set.λU,V:C squareB → Prop.
  23    λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
  24
  25 definition compose_os_relations ≝
  26   λC:ordered_set.λU,V:C squareB → Prop.
  27    λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
  28
  29 interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations ? a b).
  30 interpretation "ordered set relations composition" 'compose a b = (compose_os_relations ? a b).
  31
  32 definition invert_bs_relation ≝
  33   λC:bishop_set.λU:C squareB → Prop.
  34     λx:C squareB. U 〈\snd x,\fst x〉.
  35
  36 notation > "\inv" with precedence 60 for @{ 'invert_symbol  }.
  37 interpretation "relation invertion" 'invert a = (invert_bs_relation ? a).
  38 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?).
  39 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x).
  40
  41 alias symbol "exists" = "CProp exists".
  42 alias symbol "compose" = "bishop set relations composition".
  43 alias symbol "and" (instance 21) = "constructive and".
  44 alias symbol "and" (instance 16) = "constructive and".
  45 alias symbol "and" (instance 9) = "constructive and".
  46 record uniform_space : Type ≝ {
  47   us_carr:> bishop_set;
  48   us_unifbase: (us_carr squareB → Prop) → CProp;
  49   us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U →
  50     (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
  51   us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
  52     ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
  53   us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U →
  54     ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
  55   us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
  56 }.
  57
  58 (* Definition 2.14 *)
  59 alias symbol "leq" = "natural 'less or equal to'".
  60 definition cauchy ≝
  61   λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
  62    ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
  63
  64 notation < "a \nbsp 'is_cauchy'" non associative with precedence 45
  65   for @{'cauchy $a}.
  66 notation > "a 'is_cauchy'" non associative with precedence 45
  67   for @{'cauchy $a}.
  68 interpretation "Cauchy sequence" 'cauchy s = (cauchy ? s).
  69
  70 (* Definition 2.15 *)
  71 definition uniform_converge ≝
  72   λC:uniform_space.λa:sequence C.λu:C.
  73     ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U 〈u,a i〉.
  74
  75 notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
  76   for @{'uniform_converge $a $x}.
  77 notation > "a 'uniform_converges' x" non associative with precedence 45
  78   for @{'uniform_converge $a $x}.
  79 interpretation "Uniform convergence" 'uniform_converge s u =
  80  (uniform_converge ? s u).
  81
  82 (* Lemma 2.16 *)
  83 lemma uniform_converge_is_cauchy :
  84   ∀C:uniform_space.∀a:sequence C.∀x:C.
  85    a uniform_converges x → a is_cauchy.
  86 intros (C a x Ha); intros 2 (u Hu);
  87 cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
  88 cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
  89 apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
  90 cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
  91 apply (Hn ? H1);
  92 qed.