Section CompleteProduct.

Completion of product spaces.

This section develops the strong monad properties of the Completion operation with respect to the product operation.
Variable X Y:MetricSpace.
Let XY := ProductMS X Y.

The projection operations are uniformly continuous
Lemma fst_uc : is_UniformlyContinuousFunction (fun p:XY => fst p) Qpos2QposInf.


Definition pi1 : XY --> X :=
Build_UniformlyContinuousFunction fst_uc.

Lemma snd_uc : is_UniformlyContinuousFunction (fun p:XY => snd p) Qpos2QposInf.

Definition pi2 : XY --> Y :=
Build_UniformlyContinuousFunction snd_uc.

Definition Cfst_raw (p:Complete XY) (e:QposInf) : X :=
(fst (approximate p e)).

Definition Csnd_raw (p:Complete XY) (e:QposInf) : Y :=
(snd (approximate p e)).

Lemma Cfst_prf : forall p, is_RegularFunction (Cfst_raw p).

Lemma Csnd_prf : forall p, is_RegularFunction (Csnd_raw p).

Definition Cfst_fun (p:Complete XY) : Complete X :=
Build_RegularFunction (Cfst_prf p).

Definition Csnd_fun (p:Complete XY) : Complete Y :=
Build_RegularFunction (Csnd_prf p).

Lemma Cfst_uc : is_UniformlyContinuousFunction Cfst_fun Qpos2QposInf.

Lemma Csnd_uc : is_UniformlyContinuousFunction Csnd_fun Qpos2QposInf.

Definition Cfst : Complete XY --> Complete X :=
Build_UniformlyContinuousFunction Cfst_uc.

Definition Csnd : Complete XY --> Complete Y :=
Build_UniformlyContinuousFunction Csnd_uc.

The pairing function is uniformly continuous
Lemma pair_uc_l : forall y:Y, @is_UniformlyContinuousFunction X XY (fun x => (x,y)) Qpos2QposInf.

Lemma pair_uc_r : forall x:X, @is_UniformlyContinuousFunction Y XY (fun y => (x,y)) Qpos2QposInf.

C(X*Y) is isomorphic to (C X)*(C Y)
Definition Couple_raw (p: ProductMS (Complete X) (Complete Y)) (e:QposInf): XY :=
(approximate (fst p) e,approximate (snd p) e).

Lemma Couple_prf : forall p, is_RegularFunction (Couple_raw p).

Definition Couple_fun (p: ProductMS (Complete X) (Complete Y)) : Complete XY :=
Build_RegularFunction (Couple_prf p).

Lemma Couple_uc : is_UniformlyContinuousFunction Couple_fun Qpos2QposInf.

Definition Couple : (ProductMS (Complete X) (Complete Y)) --> (Complete (ProductMS X Y)) :=
Build_UniformlyContinuousFunction Couple_uc.

Lemma CoupleCorrect1 : forall p,
st_eq (Couple ((Cfst p), (Csnd p))) p.

Lemma CoupleCorrect2 : forall p q,
st_eq (Cfst (Couple (p,q))) p.

Lemma CoupleCorrect3 : forall p q,
st_eq (Csnd (Couple (p,q))) q.

End CompleteProduct.