Metric Space

In this version, a metric space over a setoid X is characterized by a ball relation B where B e x y is intended to mean that the two points x and y are within e of each other ( d(x,y)<=e ). This is characterized by the axioms given in the record structure below.

Record is_MetricSpace (X:Setoid) (B: Q⁺ -> relation X) : Prop :=
{ msp_refl: forall e, reflexive _ (B e)
; msp_sym: forall e, symmetric _ (B e)
; msp_triangle: forall e1 e2 a b c, B e1 a b -> B e2 b c -> B (e1 + e2)%Qpos a c
; msp_closed: forall e a b, (forall d, B (e+d)%Qpos a b) -> B e a b
; msp_eq: forall a b, (forall e, B e a b) -> st_eq a b
}.

Record MetricSpace : Type :=
{ msp_is_setoid :> Setoid
; ball : Q⁺ -> msp_is_setoid -> msp_is_setoid -> Prop
; ball_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
            forall x1 x2, (st_eq x1 x2) ->
            forall y1 y2, (st_eq y1 y2) ->
            (ball e1 x1 y1 <-> ball e2 x2 y2)
; msp : is_MetricSpace msp_is_setoid ball
}.

Section Metric_Space.

Variable X : MetricSpace.

These lemmas give direct access to the ball axioms of a metric space

Lemma ball_refl : forall e (a:X), ball e a a.

Lemma ball_sym : forall e (a b:X), ball e a b -> ball e b a.

Lemma ball_triangle : forall e1 e2 (a b c:X), ball e1 a b -> ball e2 b c -> ball (e1+e2) a c.

Lemma ball_closed : forall e (a b:X), (forall d, ball (e+d) a b) -> ball e a b.

Lemma ball_eq : forall (a b:X), (forall e, ball e a b) -> st_eq a b.

Lemma ball_eq_iff : forall (a b:X), (forall e, ball e a b) <-> st_eq a b.

The ball constraint on a and b can always be weakened. Here are two forms of the weakening lemma.

Lemma ball_weak : forall e d (a b:X), ball e a b -> ball (e+d) a b.

Lemma ball_weak_le : forall (e d:Qpos) (a b:X), e<=d -> ball e a b -> ball d a b.

End Metric_Space.