Section ProductSetoid.
Variable X Y : Setoid.
Definition prod_st_eq (a b:X*Y) :=
st_eq (fst a) (fst b) /\ st_eq (snd a) (snd b).
Lemma prodST : Setoid_Theory _ prod_st_eq.
Definition prodS : Setoid := Build_Setoid prodST.
End ProductSetoid.
Section ProductMetric.
Variable X Y : MetricSpace.
Definition prod_ball e (a b:X*Y) :=
ball e (fst a) (fst b) /\ ball e (snd a) (snd b).
Lemma prod_ball_refl : forall e a, prod_ball e a a.
Lemma prod_ball_sym : forall e a b, prod_ball e a b -> prod_ball e b a.
Lemma prod_ball_triangle : forall e1 e2 a b c, prod_ball e1 a b -> prod_ball e2 b c -> prod_ball (e1 + e2) a c.
Lemma prod_ball_closed : forall e a b, (forall d, prod_ball (e + d) a b) -> prod_ball e a b.
Lemma prod_ball_eq : forall a b, (forall e, prod_ball e a b) -> prod_st_eq _ _ a b.
Lemma prod_is_MetricSpace : is_MetricSpace (prodS X Y) prod_ball.
Definition ProductMS : MetricSpace.
Defined.
Variable X Y : Setoid.
Definition prod_st_eq (a b:X*Y) :=
st_eq (fst a) (fst b) /\ st_eq (snd a) (snd b).
Lemma prodST : Setoid_Theory _ prod_st_eq.
Definition prodS : Setoid := Build_Setoid prodST.
End ProductSetoid.
Section ProductMetric.
Variable X Y : MetricSpace.
Definition prod_ball e (a b:X*Y) :=
ball e (fst a) (fst b) /\ ball e (snd a) (snd b).
Lemma prod_ball_refl : forall e a, prod_ball e a a.
Lemma prod_ball_sym : forall e a b, prod_ball e a b -> prod_ball e b a.
Lemma prod_ball_triangle : forall e1 e2 a b c, prod_ball e1 a b -> prod_ball e2 b c -> prod_ball (e1 + e2) a c.
Lemma prod_ball_closed : forall e a b, (forall d, prod_ball (e + d) a b) -> prod_ball e a b.
Lemma prod_ball_eq : forall a b, (forall e, prod_ball e a b) -> prod_st_eq _ _ a b.
Lemma prod_is_MetricSpace : is_MetricSpace (prodS X Y) prod_ball.
Definition ProductMS : MetricSpace.
Defined.
Product metrics preserve properties of metric spaces such as
being a prelenght space, being stable, being located, and being deciable
Lemma ProductMS_prelength : PrelengthSpace X -> PrelengthSpace Y -> PrelengthSpace ProductMS.
Lemma ProductMS_stable : stableMetric X -> stableMetric Y -> stableMetric ProductMS.
Lemma ProductMS_stable : stableMetric X -> stableMetric Y -> stableMetric ProductMS.
Furthermore, if a product space is stable, then the components are
stable (assuming the components are non-zero).
Lemma ProductMS_stableX : Y -> stableMetric ProductMS -> stableMetric X.
Lemma ProductMS_stableY : X -> stableMetric ProductMS -> stableMetric Y.
Lemma ProductMS_located : locatedMetric X -> locatedMetric Y -> locatedMetric ProductMS.
Lemma ProductMS_decidable : decidableMetric X -> decidableMetric Y -> decidableMetric ProductMS.
Lemma ProductMS_stableY : X -> stableMetric ProductMS -> stableMetric Y.
Lemma ProductMS_located : locatedMetric X -> locatedMetric Y -> locatedMetric ProductMS.
Lemma ProductMS_decidable : decidableMetric X -> decidableMetric Y -> decidableMetric ProductMS.
This defines a pairing function with types of a metric space
together forms the tensor of two functions operating between
metric spaces
Lemma together_uc : forall A B C D (f:A --> C) (g:B --> D),
is_UniformlyContinuousFunction (fun (p:ProductMS A B) => (f (fst p), g (snd p)):ProductMS C D) (fun x => QposInf_min (mu f x) (mu g x)).
Definition together A B C D (f:A --> C) (g:B --> D) : (ProductMS A B --> ProductMS C D) :=
Build_UniformlyContinuousFunction (together_uc f g).
is_UniformlyContinuousFunction (fun (p:ProductMS A B) => (f (fst p), g (snd p)):ProductMS C D) (fun x => QposInf_min (mu f x) (mu g x)).
Definition together A B C D (f:A --> C) (g:B --> D) : (ProductMS A B --> ProductMS C D) :=
Build_UniformlyContinuousFunction (together_uc f g).