List and membership of lists are used in the definition of
"totally bounded". Note that we use the Leibniz equality in the definition
of MSmember, and not the setoid equality. So we are really talking about
finite sets of representants, instead of finite subsetoids. This seems to make
the proofs a bit easier.
Fixpoint MSmember (X : CSetoid) (x : X) (l : list X) {struct l} : CProp :=
match l with
| nil => ⊥
| cons y m => MSmember X x m or x = y
end.
Definition to_IR (P : IR -> CProp) : subcsetoid_crr IR P -> IR.
Defined.
Definition from_IR (P : IR -> CProp) (x : IR) (H : P x) : subcsetoid_crr IR P.
Defined.
Definition list_IR (P : IR -> CProp) :
list (SubPsMetricSpace IR_as_CPsMetricSpace P) -> list IR.
Defined.
Lemma is_P :
forall (P : IR -> CProp)
(l : list (SubPsMetricSpace IR_as_CPsMetricSpace P))
(x : IR), pred_wd IR P -> member x (list_IR P l) -> P x.
If a real number is element of a list in the above defined sense,
it is an element of the list in the sense of member,
that uses the setoid equality.
Lemma member1 :
forall (P : IR -> CProp) (x0 : subcsetoid_crr IR P)
(l : list (SubPsMetricSpace IR_as_CPsMetricSpace P)),
MSmember (X:=SubPsMetricSpace IR_as_CPsMetricSpace P) x0 l ->
member (to_IR P x0) (list_IR P l).
The image under a certain mapping of an element of a list l is member
of the list of images of elements of l.
Lemma map_member :
forall (X Z : CPsMetricSpace) (f : X -> Z) (l : list X) (m : X),
MSmember m l -> MSmember (f m) (map f l).
End lists.
Section loc_and_bound.
Definition Re_co_do (X Z : CSetoid) (f : CSetoid_fun X Z) :
X -> Build_SubCSetoid Z (fun y : Z => {x : X | f x[=]y}).
Defined.
Lemma Re_co_do_strext :
forall (X Z : CSetoid) (f : CSetoid_fun X Z),
fun_strext (Re_co_do X Z f).
Definition re_co_do (X Z : CSetoid) (f : CSetoid_fun X Z) :
CSetoid_fun X (Build_SubCSetoid Z (fun y : Z => {x : X | f x[=]y})) :=
Build_CSetoid_fun X (Build_SubCSetoid Z (fun y : Z => {x : X | f x[=]y}))
(Re_co_do X Z f) (Re_co_do_strext X Z f).
Lemma re_co_do_well_def :
forall (X Z : CSetoid) (f : CSetoid_fun X Z),
pred_wd Z (fun y : Z => {x : X | f x[=]y}).
Again we see that the image under a certain mapping of an element of a list
l is member of the list of images of elements of l.
Lemma map_member' :
forall (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (l : list X) (m : X),
MSmember m l ->
MSmember (X:=Build_SubCSetoid Z (fun y : Z => {x0 : X | f x0[=]y}))
(re_co_do X Z f m) (map (re_co_do X Z f) l).
Definition bounded (X : CPsMetricSpace) : CProp :=
{n : IR | forall x y : X, x[-d]y[<=]n}.
Definition MStotally_bounded (X : CPsMetricSpace) : CProp :=
forall n : N,
{l : list X |
forall x : X, {y : X | MSmember y l | x[-d]y[<=]one_div_succ n}}.
Total boundedness is preserved under uniformly continuous mappings.
Lemma unicon_resp_totallybounded :
forall (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (H : uni_continuous'' f),
MStotally_bounded X ->
MStotally_bounded (SubPsMetricSpace (fun y : Z => {x : X | f x[=]y})).
Lemma MStotallybounded_totallybounded :
forall (P : IR -> CProp) (H0 : {x : IR | P x}),
pred_wd IR P ->
MStotally_bounded (SubPsMetricSpace (X:=IR_as_CPsMetricSpace) P) ->
totally_bounded P.
Every image under an uniformly continuous function of an totally bounded
pseudo metric space has an infimum and a supremum.
Lemma infimum_exists :
forall (X : CPsMetricSpace) (f : CSetoid_fun X IR_as_CPsMetricSpace),
uni_continuous'' f ->
MStotally_bounded X ->
forall x : X,
{z : IR | set_glb_IR (fun y : IR_as_CPsMetricSpace => {x : X | f x[=]y}) z}.
Lemma supremum_exists :
forall (X : CPsMetricSpace) (f : CSetoid_fun X IR_as_CPsMetricSpace),
uni_continuous'' f ->
MStotally_bounded X ->
forall x : X,
{z : IR | set_lub_IR (fun y : IR_as_CPsMetricSpace => {x : X | f x[=]y}) z}.
A subspace P of a pseudo metric space X is said to be located if for all
elements x of X there exists an infimum for the distance
between x and the elements of P.
Definition located (X : CPsMetricSpace) (P : X -> CProp) :=
forall (x : X) (r : SubPsMetricSpace P),
{z : IR |
set_glb_IR
(fun v : IR => {y : SubPsMetricSpace P | dsub'_as_cs_fun P x y[=]v}) z}.
Definition located' (X : CPsMetricSpace) (P : X -> CProp) :=
forall (x : X) (y : SubPsMetricSpace P),
{z : IR |
set_glb_IR
(fun v : IR =>
{y : SubPsMetricSpace P | x[-d]from_SubPsMetricSpace X P y[=]v}) z}.
Lemma located_imp_located' :
forall (X : CPsMetricSpace) (P : X -> CProp), located P -> located' P.
Every totally bounded pseudo metric space is located.
Lemma MStotally_bounded_imp_located :
forall (X : CPsMetricSpace) (P : X -> CProp),
MStotally_bounded (SubPsMetricSpace P) -> located P.
For all x in a pseudo metric space X, for all located subspaces P of X,
Floc chooses for a given natural number n an y in P such that:
d(x,y) ≤ inf{d(x,p)| pϵP} + (n+1)-1.
Flocfun does (almost) the same, but has a different type. This enables
one to use the latter as an argument of map.
Definition Floc (X : CPsMetricSpace) (P : X -> CProp)
(H0 : located' P) (H2 : SubPsMetricSpace P) (n : N)
(x : X) :
{y : SubPsMetricSpace P |
{z : IR |
set_glb_IR
(fun v : IR =>
{y : SubPsMetricSpace P | x[-d]from_SubPsMetricSpace X P y[=]v}) z |
x[-d]from_SubPsMetricSpace X P y[<=]z[+]one_div_succ n}}.
Defined.
Definition Flocfun (X : CPsMetricSpace) (P : X -> CProp)
(H0 : located' P) (H2 : SubPsMetricSpace P) (n : N) :
X -> SubPsMetricSpace P.
Defined.
A located subset P of a totally bounded pseudo metric space
X is totally
bounded.
Lemma locatedsub_totallybounded_imp_totallyboundedsub :
forall (X : CPsMetricSpace) (P : X -> CProp),
SubPsMetricSpace P ->
located' P -> MStotally_bounded X -> MStotally_bounded (SubPsMetricSpace P).
Here are some definitions that could come in handy:
Definition MSCauchy_seq (X : CPsMetricSpace) (seq : N -> X) : CProp :=
forall n : N,
{m : N |
forall i j : N, m <= i -> m <= j -> seq i[-d]seq j[<=]one_div_succ n}.
Definition MSComplete (X : CPsMetricSpace) : CProp :=
forall seq : N -> X,
MSCauchy_seq X seq -> {lim : X | MSseqLimit' seq lim}.
A compact pseudo metric space is a pseudo metric space which is complete and
totally bounded.
A subset P is open if for all x in P there exists an open sphere
with centre x that is contained in P.
Definition open (X : CPsMetricSpace) (P : X -> CProp) :=
forall x : X,
P x -> {e : IR | 0[<]e and (forall z : X, z[-d]x[<]e -> P z)}.
The operator infima gives the infimum for the distance between an
element x of a located pseudo metric space X and the elements of a
subspace P of X.
Definition infima (X : CPsMetricSpace) (P : X -> CProp)
(H : located' P) (a : SubPsMetricSpace P) : X -> IR.
Defined.
A non-empty totally bounded sub-pseudo-metric-space P is said to be
well contained in an open sub-pseudo-metric-space Q if Q contains
all points that are in some sense close to P.
Definition well_contained (X : CPsMetricSpace) (P Q : X -> CProp)
(a : SubPsMetricSpace P) :=
open Q ->
forall H : MStotally_bounded (SubPsMetricSpace P),
{r : IR | 0[<]r |
forall q : X,
infima P (located_imp_located' X P (MStotally_bounded_imp_located X P H)) a
q[<=]r -> Q q}.
End loc_and_bound.