Relations necessary for Pseudo Metric Spaces and Metric Spaces
Let A : CSetoid, d : (CSetoid_bin_fun A A IR).
Variable A : CSetoid.
Variable d : CSetoid_bin_fun A A IR.
Definition com : Prop := forall x y : A, d x y[=]d y x.
Definition nneg : Prop := forall x y : A, 0[<=]d x y.
Definition pos_imp_ap : CProp := forall x y : A, 0[<]d x y -> x[#]y.
Definition tri_ineq : Prop := forall x y z : A, d x z[<=]d x y[+]d y z.
Definition diag_zero (X : CSetoid) (d : CSetoid_bin_fun X X IR) : Prop :=
forall x : X, d x x[=]0.
Definition apdiag_imp_grzero (X : CSetoid) (d : CSetoid_bin_fun X X IR) :
CProp := forall x y : X, x[#]y -> 0[<]d x y.
End Relations.
Section Definition_PsMS0.
Variable d : CSetoid_bin_fun A A IR.
Definition com : Prop := forall x y : A, d x y[=]d y x.
Definition nneg : Prop := forall x y : A, 0[<=]d x y.
Definition pos_imp_ap : CProp := forall x y : A, 0[<]d x y -> x[#]y.
Definition tri_ineq : Prop := forall x y z : A, d x z[<=]d x y[+]d y z.
Definition diag_zero (X : CSetoid) (d : CSetoid_bin_fun X X IR) : Prop :=
forall x : X, d x x[=]0.
Definition apdiag_imp_grzero (X : CSetoid) (d : CSetoid_bin_fun X X IR) :
CProp := forall x y : X, x[#]y -> 0[<]d x y.
End Relations.
Section Definition_PsMS0.
A pseudo metric space consists of a setoid and a "pseudo metric", also called
"distance", a binairy function that fulfils certain properties.
Record is_CPsMetricSpace (A : CSetoid) (d : CSetoid_bin_fun A A IR) :
Type :=
{ax_d_com : com d;
ax_d_nneg : nneg d;
ax_d_pos_imp_ap : pos_imp_ap d;
ax_d_tri_ineq : tri_ineq d}.
Record CPsMetricSpace : Type :=
{cms_crr :> CSetoid;
cms_d : CSetoid_bin_fun cms_crr cms_crr IR;
cms_proof : is_CPsMetricSpace cms_crr cms_d}.
End Definition_PsMS0.
Infix "[-d]" := cms_d (at level 68, left associativity).
Section PsMS_axioms.
Variable A : CPsMetricSpace.
Lemma CPsMetricSpace_is_CPsMetricSpace : is_CPsMetricSpace A cms_d.
Lemma d_com : com (cms_d (c:=A)).
Lemma d_nneg : nneg (cms_d (c:=A)).
Lemma d_pos_imp_ap : pos_imp_ap (cms_d (c:=A)).
Lemma d_tri_ineq : tri_ineq (cms_d (c:=A)).
End PsMS_axioms.
Section PsMS_basics.
Lemma CPsMetricSpace_is_CPsMetricSpace : is_CPsMetricSpace A cms_d.
Lemma d_com : com (cms_d (c:=A)).
Lemma d_nneg : nneg (cms_d (c:=A)).
Lemma d_pos_imp_ap : pos_imp_ap (cms_d (c:=A)).
Lemma d_tri_ineq : tri_ineq (cms_d (c:=A)).
End PsMS_axioms.
Section PsMS_basics.
Variable Y : CPsMetricSpace.
Lemma rev_tri_ineq :
forall a b c : cms_crr Y, AbsSmall (b[-d]c) ((a[-d]b)[-](a[-d]c)).
Instead of taking pos_imp_ap as axiom,
we could as well have taken diag_zero.
Lemma diag_zero_imp_pos_imp_ap :
forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
diag_zero X d -> pos_imp_ap d.
Lemma pos_imp_ap_imp_diag_zero :
forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
pos_imp_ap d -> nneg d -> diag_zero X d.
Lemma is_CPsMetricSpace_diag_zero :
forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
com d /\ tri_ineq d /\ nneg d /\ diag_zero X d -> is_CPsMetricSpace X d.
End PsMS_basics.
Section Zerof.
Every setoid forms with the binary function that always returns zero,
a pseudo metric space.
Definition zero_fun (X : CSetoid) (x y : X) : IR := 0.
Lemma zero_fun_strext :
forall X : CSetoid, bin_fun_strext X X IR (zero_fun X).
Definition Zero_fun (X : CSetoid) :=
Build_CSetoid_bin_fun X X IR (zero_fun X) (zero_fun_strext X).
Lemma zero_fun_com : forall X : CSetoid, com (Zero_fun X).
Lemma zero_fun_nneg : forall X : CSetoid, nneg (Zero_fun X).
Lemma zero_fun_pos_imp_ap : forall X : CSetoid, pos_imp_ap (Zero_fun X).
Lemma zero_fun_tri_ineq : forall X : CSetoid, tri_ineq (Zero_fun X).
Definition zf_is_CPsMetricSpace (X : CSetoid) :=
Build_is_CPsMetricSpace X (Zero_fun X) (zero_fun_com X) (
zero_fun_nneg X) (zero_fun_pos_imp_ap X) (zero_fun_tri_ineq X).
Definition zf_as_CPsMetricSpace (X : CSetoid) :=
Build_CPsMetricSpace X (Zero_fun X) (zf_is_CPsMetricSpace X).
End Zerof.