Let X be a pseudo metric space.
The real numbers with the usual distance form a pseudo metric space.
Definition dIR (x y : IR) : IR := ABSIR (x[-]y).
Lemma bin_fun_strext_dIR : bin_fun_strext IR IR IR dIR.
Definition dIR_as_CSetoid_fun :=
Build_CSetoid_bin_fun IR IR IR dIR bin_fun_strext_dIR.
Lemma dIR_nneg : forall x y : IR, 0[<=]dIR_as_CSetoid_fun x y.
Lemma dIR_com :
forall x y : IR, dIR_as_CSetoid_fun x y[=]dIR_as_CSetoid_fun y x.
Lemma dIR_pos_imp_ap :
forall x y : IR, 0[<]dIR_as_CSetoid_fun x y -> x[#]y.
Lemma dIR_tri_ineq : tri_ineq dIR_as_CSetoid_fun.
Definition IR_dIR_is_CPsMetricSpace :=
Build_is_CPsMetricSpace IR dIR_as_CSetoid_fun dIR_com dIR_nneg
dIR_pos_imp_ap dIR_tri_ineq.
Definition IR_as_CPsMetricSpace :=
Build_CPsMetricSpace IR dIR_as_CSetoid_fun IR_dIR_is_CPsMetricSpace.
Variable X : CPsMetricSpace.
Lemma rev_tri_ineq' :
forall a b c : X,
cms_d (c:=IR_as_CPsMetricSpace) (a[-d]b) (a[-d]c)[<=]b[-d]c.
A pseudo metric is Lipschitz. Hence it is uniformly continuous and continuous.
Lemma d_is_lipschitz :
forall a : X,
lipschitz (projected_bin_fun X X IR_as_CPsMetricSpace (cms_d (c:=X)) a).
Lemma d_is_uni_continuous :
forall a : X,
uni_continuous (projected_bin_fun X X IR_as_CPsMetricSpace (cms_d (c:=X)) a).
Lemma d_is_continuous :
forall a : X,
continuous (projected_bin_fun X X IR_as_CPsMetricSpace (cms_d (c:=X)) a).
End Reals.
Section Addition.
The sum of two Lipschitz/uniformly continous/continuous functions is again
Lipschitz/uniformly continuous/continuous.
Lemma plus_resp_lipschitz :
forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace)
(H : lipschitz f) (H1 : lipschitz g),
lipschitz
(compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g
(csg_op (c:=IR))).
Lemma plus_resp_uni_continuous :
forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace)
(H : uni_continuous f) (H1 : uni_continuous g),
uni_continuous
(compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g
(csg_op (c:=IR))).
Lemma plus_resp_continuous :
forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace)
(H : continuous f) (H1 : continuous g),
continuous
(compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g
(csg_op (c:=IR))).
End Addition.