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".
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;]]
28 definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
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).
35 notation "hvbox({ ident x : t | break 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).
41 notation < "s 2 \atop \neq" non associative with precedence 90
43 notation > "s 'square'" non associative with precedence 90
45 interpretation "bishop set square" 'square x =
46 (cic:/matita/dama/uniform/square_bishop_set.con x).
47 interpretation "bishop set square" 'square2 x =
48 (cic:/matita/dama/uniform/square_bishop_set.con x).
51 alias symbol "exists" = "exists".
52 alias symbol "and" = "logical and".
53 definition compose_relations ≝
54 λC:bishop_set.λU,V:C square → Prop.
55 λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
57 notation "a \circ b" left associative with precedence 60
58 for @{'compose $a $b}.
59 interpretation "relations composition" 'compose a b =
60 (cic:/matita/dama/uniform/compose_relations.con _ a b).
61 notation "hvbox(x \in break a \circ break b)" non associative with precedence 50
62 for @{'compose2 $a $b $x}.
63 interpretation "relations composition" 'compose2 a b x =
64 (cic:/matita/dama/uniform/compose_relations.con _ a b x).
66 definition invert_relation ≝
67 λC:bishop_set.λU:C square → Prop.
68 λx:C square. U 〈snd x,fst x〉.
70 notation < "s \sup (-1)" non associative with precedence 90
72 notation < "s \sup (-1) x" non associative with precedence 90
73 for @{ 'invert2 $s $x}.
74 notation > "'inv' s" non associative with precedence 90
76 interpretation "relation invertion" 'invert a =
77 (cic:/matita/dama/uniform/invert_relation.con _ a).
78 interpretation "relation invertion" 'invert2 a x =
79 (cic:/matita/dama/uniform/invert_relation.con _ a x).
81 alias symbol "exists" = "CProp exists".
82 alias symbol "and" (instance 18) = "constructive and".
83 alias symbol "and" (instance 10) = "constructive and".
84 record uniform_space : Type ≝ {
86 us_unifbase: (us_carr square → Prop) → CProp;
87 us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
88 {x:us_carr square|fst x ≈ snd x} ⊆ U;
89 us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
90 ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
91 us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
92 ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
93 us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
97 alias symbol "leq" = "natural 'less or equal to'".
99 λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
100 ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
102 notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
104 notation > "a 'is_cauchy'" non associative with precedence 50
106 interpretation "Cauchy sequence" 'cauchy s =
107 (cic:/matita/dama/uniform/cauchy.con _ s).
109 (* Definition 2.15 *)
110 definition uniform_converge ≝
111 λC:uniform_space.λa:sequence C.λu:C.
112 ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
114 notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
115 for @{'uniform_converge $a $x}.
116 notation > "a 'uniform_converges' x" non associative with precedence 50
117 for @{'uniform_converge $a $x}.
118 interpretation "Uniform convergence" 'uniform_converge s u =
119 (cic:/matita/dama/uniform/uniform_converge.con _ s u).
122 lemma uniform_converge_is_cauchy :
123 ∀C:uniform_space.∀a:sequence C.∀x:C.
124 a uniform_converges x → a is_cauchy.
125 intros (C a x Ha); intros 2 (u Hu);
126 cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
127 cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
128 apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
129 cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
133 (* Definition 2.17 *)
134 definition mk_big_set ≝
135 λP:CProp.λF:P→CProp.F.
136 interpretation "explicit big set" 'explicitset t =
137 (cic:/matita/dama/uniform/mk_big_set.con _ t).
139 definition restrict_uniformity ≝
140 λC:uniform_space.λX:C→Prop.
141 {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.