The product metric here defined is:
dprod((a1,b1),(a2,b2)):= dA(a1,b1)+dB(b1,b2).
This is not the one used to make the metric of
IR2 out of the metric of IR.
Definition dprod0 (A B : CPsMetricSpace) (c d : prodT A B) : IR.
Defined.
Lemma dprod0_strext :
forall A B : CPsMetricSpace,
bin_fun_strext (ProdCSetoid A B) (ProdCSetoid A B) IR (dprod0 A B).
Definition d_prod0 (A B : CPsMetricSpace) :=
Build_CSetoid_bin_fun (ProdCSetoid A B) (ProdCSetoid A B) IR (
dprod0 A B) (dprod0_strext A B).
Lemma prod0cpsmetricspace_is_CPsMetricSpace :
forall A B : CPsMetricSpace,
is_CPsMetricSpace (ProdCSetoid A B) (d_prod0 A B).
Definition Prod0CPsMetricSpace (A B : CPsMetricSpace) :=
Build_CPsMetricSpace (ProdCSetoid A B) (d_prod0 A B)
(prod0cpsmetricspace_is_CPsMetricSpace A B).
End prodpsmetrics.
Section subpsmetrics.
The pseudo metric on a subspace Y of a pseudo metric space X is
the pseudo metric on X restricted to Y.
Definition restr_bin_fun (X : CPsMetricSpace) (P : cms_crr X -> CProp)
(f : CSetoid_bin_fun X X IR) (a b : Build_SubCSetoid X P) : IR :=
match a, b with
| Build_subcsetoid_crr x p, Build_subcsetoid_crr y q => f x y
end.
Definition restr_bin_fun' (X : CPsMetricSpace) (P : cms_crr X -> CProp)
(f : CSetoid_bin_fun X X IR) (a : X) (b : Build_SubCSetoid X P) : IR :=
match b with
| Build_subcsetoid_crr y q => f a y
end.
Lemma restr_bin_fun_strext :
forall (X : CPsMetricSpace) (P : cms_crr X -> CProp)
(f : CSetoid_bin_fun X X IR),
bin_fun_strext (Build_SubCSetoid X P) (Build_SubCSetoid X P) IR
(restr_bin_fun P f).
Definition Build_SubCSetoid_bin_fun (X : CPsMetricSpace)
(P : cms_crr X -> CProp) (f : CSetoid_bin_fun X X IR) :
CSetoid_bin_fun (Build_SubCSetoid X P) (Build_SubCSetoid X P) IR :=
Build_CSetoid_bin_fun (Build_SubCSetoid X P) (Build_SubCSetoid X P) IR
(restr_bin_fun P f) (restr_bin_fun_strext X P f).
Definition dsub (X : CPsMetricSpace) (P : cms_crr X -> CProp) :=
Build_SubCSetoid_bin_fun X P (cms_d (c:=X)).
Lemma dsub_com :
forall (X : CPsMetricSpace) (P : cms_crr X -> CProp), com (dsub P).
Lemma dsub_nneg :
forall (X : CPsMetricSpace) (P : cms_crr X -> CProp), nneg (dsub P).
Lemma dsub_pos_imp_ap :
forall (X : CPsMetricSpace) (P : cms_crr X -> CProp), pos_imp_ap (dsub P).
Lemma dsub_tri_ineq :
forall (X : CPsMetricSpace) (P : cms_crr X -> CProp), tri_ineq (dsub P).
Definition is_SubPsMetricSpace (X : CPsMetricSpace)
(P : cms_crr X -> CProp) :
is_CPsMetricSpace (Build_SubCSetoid X P) (dsub P) :=
Build_is_CPsMetricSpace (Build_SubCSetoid X P) (dsub P) (
dsub_com X P) (dsub_nneg X P) (dsub_pos_imp_ap X P) (
dsub_tri_ineq X P).
Definition SubPsMetricSpace (X : CPsMetricSpace) (P : cms_crr X -> CProp) :
CPsMetricSpace :=
Build_CPsMetricSpace (Build_SubCSetoid X P) (dsub P)
(is_SubPsMetricSpace X P).
Definition from_SubPsMetricSpace (X : CPsMetricSpace)
(P : X -> CProp) : SubPsMetricSpace P -> X.
Defined.
The function dsub' is used in the definition of "located".
It enables one to speak about a distance between an element of a
pseudo metric space and a certain subspace.
Definition dsub' (X : CPsMetricSpace) (P : X -> CProp)
(x : X) (y : SubPsMetricSpace P) := from_SubPsMetricSpace X P y[-d]x.
Lemma dsub'_strext :
forall (X : CPsMetricSpace) (P : X -> CProp) (x : X),
fun_strext (dsub' P x).
Definition dsub'_as_cs_fun (X : CPsMetricSpace) (P : X -> CProp)
(x : X) :=
Build_CSetoid_fun (SubPsMetricSpace P) IR_as_CPsMetricSpace (
dsub' P x) (dsub'_strext X P x).
Lemma dsub'_uni_continuous'' :
forall (X : CPsMetricSpace) (P : X -> CProp) (x : X),
uni_continuous'' (dsub'_as_cs_fun P x).
End subpsmetrics.