Record CMetricSpace : Type :=
{scms_crr :> CPsMetricSpace;
ax_d_apdiag_imp_grzero : apdiag_imp_grzero scms_crr (cms_d (c:=scms_crr))}.
End Definition_MS.
Section MS_basics.
Lemma d_CMetricSpace_apdiag_imp_grzero :
forall X : CMetricSpace, apdiag_imp_grzero (cms_crr X) (cms_d (c:=X)).
Lemma d_zero_imp_eq :
forall (X : CMetricSpace) (a b : X), a[-d]b[=]0 -> a[=]b.
Lemma is_CMetricSpace_diag_zero :
forall (X : CSetoid) (d : CSetoid_bin_fun X X IR)
(H : com d) (H1 : tri_ineq d) (H2 : nneg d) (H3 : diag_zero X d)
(H4 : apdiag_imp_grzero X d), CMetricSpace.
End MS_basics.
Section prodandsub.
The product of two metric spaces is again a metric space.
Lemma Prod0CMetricSpaces_apdiag_grzero :
forall X Y : CMetricSpace,
apdiag_imp_grzero (Prod0CPsMetricSpace X Y)
(cms_d (c:=Prod0CPsMetricSpace X Y)).
Definition Prod0CMetricSpace (X Y : CMetricSpace) :=
Build_CMetricSpace (Prod0CPsMetricSpace X Y)
(Prod0CMetricSpaces_apdiag_grzero X Y).
A subspace of a metric space is again a metric space.
Lemma SubMetricSpace_apdiag_grzero :
forall (X : CMetricSpace) (P : X -> CProp),
apdiag_imp_grzero (SubPsMetricSpace P) (cms_d (c:=SubPsMetricSpace P)).
Definition SubMetricSpace (X : CMetricSpace) (P : X -> CProp) :=
Build_CMetricSpace (SubPsMetricSpace P) (SubMetricSpace_apdiag_grzero X P).
End prodandsub.
Section Zeroff.
Not all pseudo metric spaces are a metric space:
Lemma zf_nis_CMetricSpace :
forall X : CSetoid,
{x : X | {y : X | x[#]y}} ->
~
(apdiag_imp_grzero (zf_as_CPsMetricSpace X)
(cms_d (c:=zf_as_CPsMetricSpace X))).
But a pseudo metric space induces a metric space:
Definition metric_ap (X : CPsMetricSpace) (x y : X) : CProp := 0[<]x[-d]y.
Definition metric_eq (X : CPsMetricSpace) (x y : X) : Prop := x[-d]y[=]0.
Lemma metric_ap_irreflexive :
forall X : CPsMetricSpace, irreflexive (metric_ap X).
Lemma metric_ap_symmetric :
forall X : CPsMetricSpace, Csymmetric (metric_ap X).
Lemma metric_ap_cotransitive :
forall X : CPsMetricSpace, cotransitive (metric_ap X).
Lemma metric_ap_tight :
forall X : CPsMetricSpace, tight_apart (metric_eq X) (metric_ap X).
Definition Metric_CSet_is_CSetoid (X : CPsMetricSpace) :=
Build_is_CSetoid X (metric_eq X) (metric_ap X) (metric_ap_irreflexive X)
(metric_ap_symmetric X) (metric_ap_cotransitive X) (
metric_ap_tight X).
Definition Metric_CSetoid (X : CPsMetricSpace) :=
Build_CSetoid X (metric_eq X) (metric_ap X) (Metric_CSet_is_CSetoid X).
Definition metric_d (X : CPsMetricSpace) (x y : Metric_CSetoid X) := x[-d]y.
Lemma metric_d_strext :
forall X : CPsMetricSpace,
bin_fun_strext (Metric_CSetoid X) (Metric_CSetoid X) IR (metric_d X).
Definition Metric_d (X : CPsMetricSpace) :=
Build_CSetoid_bin_fun (Metric_CSetoid X) (Metric_CSetoid X) IR (
metric_d X) (metric_d_strext X).
Lemma Metric_d_com : forall X : CPsMetricSpace, com (Metric_d X).
Lemma Metric_d_nneg : forall X : CPsMetricSpace, nneg (Metric_d X).
Lemma Metric_d_pos_imp_ap :
forall X : CPsMetricSpace, pos_imp_ap (Metric_d X).
Lemma Metric_d_tri_ineq : forall X : CPsMetricSpace, tri_ineq (Metric_d X).
Definition QuotientCSetoid_is_CPsMetricSpace (X : CPsMetricSpace) :=
Build_is_CPsMetricSpace (Metric_CSetoid X) (Metric_d X) (
Metric_d_com X) (Metric_d_nneg X) (Metric_d_pos_imp_ap X)
(Metric_d_tri_ineq X).
Definition QuotientCPsMetricSpace (X : CPsMetricSpace) :=
Build_CPsMetricSpace (Metric_CSetoid X) (Metric_d X)
(QuotientCSetoid_is_CPsMetricSpace X).
Lemma Metric_d_apdiag_grzero :
forall X : CPsMetricSpace,
apdiag_imp_grzero (QuotientCPsMetricSpace X)
(cms_d (c:=QuotientCPsMetricSpace X)).
Definition QuotientCMetricSpace (X : CPsMetricSpace) :=
Build_CMetricSpace (QuotientCPsMetricSpace X) (Metric_d_apdiag_grzero X).
Some pseudo metric spaces already are a metric space:
Lemma dIR_apdiag_grzero :
apdiag_imp_grzero IR_as_CPsMetricSpace (cms_d (c:=IR_as_CPsMetricSpace)).
Definition IR_as_CMetricSpace :=
Build_CMetricSpace IR_as_CPsMetricSpace dIR_apdiag_grzero.
In that case the induced metric space is equivalent to the original one:
Definition emb (X : CPsMetricSpace) : X -> QuotientCMetricSpace X.
Defined.
Lemma emb_strext : forall X : CPsMetricSpace, fun_strext (emb X).
Definition Emb (X : CPsMetricSpace) :=
Build_CSetoid_fun X (QuotientCMetricSpace X) (emb X) (emb_strext X).
Lemma Quotient_pres_CMetricSpace :
forall X : CMetricSpace, isopsmetry X (QuotientCPsMetricSpace X) (Emb X).
End Zeroff.
Section Limitt.
A sequence in a metric space has at most one limit.
Lemma unique_MSseqLim :
forall (X : CMetricSpace) (seq : N -> X) (a b : X),
MSseqLimit seq a and MSseqLimit seq b -> a[=]b.
End Limitt.