This extended notition of ball operates over QposInf, allowing one to say, ball Infinity a b, holds for all a and b.

Definition ball_ex (X:MetricSpace) (e:QposInf) (a b:X) :=
 match e with
  | Qpos2QposInf e' => ball e' a b
  | ∞ => True
 end.
Lemma ball_ex_weak_le : forall (X:MetricSpace) (e d:QposInf) (a b:X), QposInf_le e d -> ball_ex e a b -> ball_ex d a b.

Lemma ball_ex_dec : forall (X:MetricSpace), (forall e (a b:X), {ball e a b}+{~ball e a b}) -> forall e (a b:X), {ball_ex e a b}+{~ball_ex e a b}.

Section UniformlyContinuousFunction.

Uniform Continuity


Variable X Y : MetricSpace.

This is the traditional definitition of uniform continuity with an explicitly given modulus of continuity
Definition is_UniformlyContinuousFunction
 (f: X -> Y) (mu: Q+ -> Q+∞) :=
 forall e a b, ball_ex (mu e) a b -> ball e (f a) (f b).

Every uniformly continuous function is automatically well defined
Lemma is_UniformlyContinuousFunction_wd : forall (f1 f2:X -> Y) (mu1 mu2: Q+ -> Q+∞),
 (forall x, st_eq (f1 x) (f2 x)) ->
 (forall x, QposInf_le (mu2 x) (mu1 x)) ->
 (is_UniformlyContinuousFunction f1 mu1) ->
 (is_UniformlyContinuousFunction f2 mu2).

A uniformly continuous function consists of a function, a modulus of continuity, and a proof that the function is uniformly continuous with that modulus
Record UniformlyContinuousFunction : Type :=
{ucFun :> X -> Y
;mu : Q+ -> Q+∞
;uc_prf : is_UniformlyContinuousFunction ucFun mu
}.

Given a uniformly continuous function with a modulus mu, it is also uniformly continuous with any smaller modulus
Lemma uc_prf_smaller : forall (f:UniformlyContinuousFunction) (mu2 : Q+ -> Q+∞),
 (forall e, QposInf_le (mu2 e) (mu f e)) ->
 is_UniformlyContinuousFunction (ucFun f) mu2.

The metric space of uniformly continuous functions

The space of uniformly continuous functions from a metric space
Definition ucEq (f g : UniformlyContinuousFunction) :=
 forall x, st_eq (f x) (g x).

Lemma uc_setoid : Setoid_Theory UniformlyContinuousFunction ucEq.

Definition uc_Setoid : Setoid := (Build_Setoid uc_setoid).

Definition ucBall e (f g : UniformlyContinuousFunction) := forall a, ball e (f a) (g a).

Lemma uc_is_MetricSpace : is_MetricSpace uc_Setoid ucBall.

Lemma ucBall_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
            forall (x1 x2 : uc_Setoid), (st_eq x1 x2) ->
            forall (y1 y2 : uc_Setoid), (st_eq y1 y2) ->
            (ucBall e1 x1 y1 <-> ucBall e2 x2 y2).

End UniformlyContinuousFunction.


Definition UniformlyContinuousSpace (X Y:MetricSpace) : MetricSpace :=
Build_MetricSpace (@ucBall_wd X Y) (@uc_is_MetricSpace X Y).

Notation "x --> y" := (UniformlyContinuousSpace x y) (at level 55, right associativity) : uc_scope.

The category of metric spaces.

Metric spaces with uniformly continuous functions form a category.

The identity function is uniformly continuous.
Lemma uc_id_prf (X:MetricSpace) : is_UniformlyContinuousFunction (fun (x:X) => x) Qpos2QposInf.

Definition uc_id (X:MetricSpace) : UniformlyContinuousFunction X X :=
Build_UniformlyContinuousFunction (uc_id_prf X).

The composition of two uniformly continuous functions is uniformly continuous
Lemma uc_compose_prf (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) :
is_UniformlyContinuousFunction (fun x => g (f x)) (fun e => QposInf_bind (mu f) (mu g e)).

Definition uc_compose (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) : X --> Z :=
Build_UniformlyContinuousFunction (uc_compose_prf g f).


Notation "f ∘ g" := (uc_compose f g) (at level 40, left associativity) : uc_scope.

Lemma is_uc_uc_compose0 : forall X Y Z (f:Y-->Z),
 is_UniformlyContinuousFunction (@uc_compose X Y Z f) (mu f).

Definition uc_compose_uc0 X Y Z (f:Y-->Z) : (X-->Y) --> X --> Z :=
 Build_UniformlyContinuousFunction (is_uc_uc_compose0 f).

Lemma is_uc_uc_compose : forall X Y Z,
 is_UniformlyContinuousFunction (@uc_compose_uc0 X Y Z) Qpos2QposInf.

Definition uc_compose_uc X Y Z : (Y-->Z)-->(X-->Y)-->X-->Z :=
 Build_UniformlyContinuousFunction (@is_uc_uc_compose X Y Z).