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 "supremum.ma".
19 alias symbol "square" = "bishop set square".
20 alias symbol "pair" = "pair".
21 alias symbol "exists" = "exists".
22 alias symbol "and" = "logical and".
23 definition compose_bs_relations ≝
24 λC:bishop_set.λU,V:C square → Prop.
25 λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
27 definition compose_os_relations ≝
28 λC:ordered_set.λU,V:C square → Prop.
29 λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
31 interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
32 interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
34 definition invert_bs_relation ≝
35 λC:bishop_set.λU:C square → Prop.
36 λx:C square. U 〈snd x,fst x〉.
38 notation < "s \sup (-1)" left associative with precedence 70
40 notation < "s \sup (-1) x" left associative with precedence 70
41 for @{ 'invert_appl $s $x}.
42 notation > "'inv'" right associative with precedence 70
43 for @{ 'invert_symbol }.
44 interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
45 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
46 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
48 alias symbol "exists" = "CProp exists".
49 alias symbol "compose" = "bishop set relations composition".
50 alias symbol "and" (instance 21) = "constructive and".
51 alias symbol "and" (instance 16) = "constructive and".
52 alias symbol "and" (instance 9) = "constructive and".
53 record uniform_space : Type ≝ {
55 us_unifbase: (us_carr square → Prop) → CProp;
56 us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
57 (λx:us_carr square.fst x ≈ snd x) ⊆ U;
58 us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
59 ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
60 us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
61 ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
62 us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
66 alias symbol "leq" = "natural 'less or equal to'".
68 λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
69 ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
71 notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
73 notation > "a 'is_cauchy'" non associative with precedence 50
75 interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
78 definition uniform_converge ≝
79 λC:uniform_space.λa:sequence C.λu:C.
80 ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
82 notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
83 for @{'uniform_converge $a $x}.
84 notation > "a 'uniform_converges' x" non associative with precedence 50
85 for @{'uniform_converge $a $x}.
86 interpretation "Uniform convergence" 'uniform_converge s u =
87 (uniform_converge _ s u).
90 lemma uniform_converge_is_cauchy :
91 ∀C:uniform_space.∀a:sequence C.∀x:C.
92 a uniform_converges x → a is_cauchy.
93 intros (C a x Ha); intros 2 (u Hu);
94 cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
95 cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
96 apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
97 cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;