-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCompletion.v
177 lines (169 loc) · 4.67 KB
/
Completion.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
Require Export Completeness.
Lemma completion_exists: forall (X:Type) (d:X->X->R) (d_metric:metric d),
exists Y:Type, exists i:X->Y, exists d':Y->Y->R,
exists d'_metric:metric d',
injective i /\ dense (Im Full_set i) (X:=MetricTopology d' d'_metric) /\
(forall x1 x2:X, d' (i x1) (i x2) = d x1 x2) /\
complete d' d'_metric.
Proof.
intros.
(* first of all, it suffices to construct a (Y, d') without the
density condition; then the restriction of d' to the closure of X
is again complete, and X is dense in it *)
cut (exists Y:Type, exists i:X->Y, exists d':Y->Y->R,
exists d'_metric:metric d', injective i /\
(forall x1 x2:X, d' (i x1) (i x2) = d x1 x2) /\
complete d' d'_metric).
intros.
destruct H as [Y [i [d' [d'_metric [? []]]]]].
pose (F := closure (Im Full_set i) (X:=MetricTopology d' d'_metric)).
exists {y:Y | In F y}.
assert (forall x:X, In F (i x)).
intros.
apply closure_inflationary.
exists x; trivial.
constructor.
exists (fun x:X => exist _ (i x) (H2 x)).
exists (fun y1 y2 => d' (proj1_sig y1) (proj1_sig y2)).
assert (d'_metric0 : metric (fun (y1 y2:{y:Y | In F y}) =>
d' (proj1_sig y1) (proj1_sig y2))).
constructor; try destruct x; try destruct y; try destruct z; simpl;
try apply d'_metric.
intros.
Require Import Proj1SigInjective.
apply subset_eq_compatT.
apply d'_metric; trivial.
exists d'_metric0.
repeat split.
red; intros.
injection H3; intros.
apply H; trivial.
red.
apply Extensionality_Ensembles; split; red; intros.
constructor.
simpl in x.
destruct x.
clear H3.
generalize i0.
apply first_countable_sequence_closure in i0.
destruct i0.
destruct H3.
assert (forall n:nat, { x:X | x0 n = i x }).
intros.
Require Import Description.
apply constructive_definite_description.
apply -> unique_existence.
split.
destruct (H3 n).
exists x1; trivial.
red; intros.
apply H.
rewrite H5 in H6; trivial.
assert (forall n:nat, In F (i (proj1_sig (X0 n)))).
intros; apply H2.
intros.
apply (@net_limit_in_closure nat_DS
(MetricTopology _ d'_metric0)
_ (fun n:nat => exist _ (i (proj1_sig (X0 n))) (H5 n))).
red; intros.
exists i1.
split.
simpl; auto with arith.
exists (proj1_sig (X0 i1)).
constructor.
apply subset_eq_compatT.
reflexivity.
pose proof (metric_space_net_limit_converse (MetricTopology d' d'_metric) d'
(MetricTopology_metrizable _ d' d'_metric) nat_DS x0 x H4).
apply metric_space_net_limit with (1:=MetricTopology_metrizable _ _ d'_metric0).
(*
destruct (metric_space_net_limit (MetricTopology d' d'_metric)
d' (MetricTopology_metrizable _ d' d'_metric) nat_DS x0 x).
pose proof (H6 H4); clear H6 H7.
apply <- (metric_space_net_limit (MetricTopology _ d'_metric0)
_ (MetricTopology_metrizable _ _ d'_metric0) nat_DS). *)
intros.
destruct (H6 eps H7).
exists x1.
intros.
simpl.
destruct (X0 j).
simpl.
rewrite <- e.
apply H8; trivial.
apply metrizable_impl_first_countable.
exists d'; trivial.
apply MetricTopology_metrizable.
intros.
simpl.
apply H0.
apply (closed_subset_of_complete_is_complete Y d' d'_metric F);
trivial.
apply closure_closed.
destruct (classic (inhabited X)).
destruct H as [x0].
(* we now construct Y as the uniform space of functions X->R,
with base point "distance from x0"; the embedding of X into this
space is to send x to "distance from x" *)
Require Import UniformTopology.
Require Import RTopology.
assert (forall x y z:X, R_metric (d x z) (d y z) <= d x y).
unfold R_metric.
assert (forall a b:R, -b <= a -> a <= b -> Rabs a <= b).
intros.
unfold Rabs.
Require Import Fourier.
destruct Rcase_abs; fourier.
intros.
apply H.
assert (d x z <= d x y + d y z) by apply d_metric.
fourier.
rewrite (metric_sym _ _ d_metric x y).
assert (d y z <= d y x + d x z) by apply d_metric.
fourier.
exists (uniform_space R_metric (d x0)).
refine (let H:=_ in ex_intro _ (fun x:X => exist _ (d x) (H x)) _).
intros.
exists (d x0 x).
red; intros.
destruct H0.
rewrite H1; trivial.
exists (uniform_metric R_metric (d x0) R_metric_is_metric
(inhabits x0)).
exists (uniform_metric_is_metric _ _ _ _ _ _).
repeat split.
red; intros.
injection H1; intros.
apply d_metric.
rewrite H2; apply d_metric.
intros.
unfold uniform_metric; destruct sup; simpl.
apply Rle_antisym.
apply i.
red; intros.
destruct H1.
rewrite H2; apply H.
apply i.
exists x1.
constructor.
rewrite metric_zero; trivial.
unfold R_metric.
rewrite (metric_sym _ _ d_metric x2 x1).
rewrite Rminus_0_r.
symmetry; apply Rabs_right; apply d_metric.
apply uniform_metric_complete.
exact R_metric_complete.
exists False.
exists (fun x:X => H (inhabits x)).
exists (False_rect _).
assert (metric (False_rect (False->R))).
constructor; intros; destruct x.
exists H0.
repeat split.
red; intros.
contradiction (H (inhabits x1)).
intros.
contradiction (H (inhabits x1)).
red; intros.
contradiction (x O).
Qed.