CoRN.reals.fast.CRconst

Require Import Unicode.Utf8 Qmetric CRmetric UniformContinuity.

Section const_fun_uc.
 Variable X : MetricSpace.
 Variable c : X.

The uniformly continuous constant function
 Definition const_raw : X → Complete X := λ _, Cunit c.

 Definition const_mu (ε:Qpos) : QposInf := QposInfinity.

 Lemma const_uc_prf : is_UniformlyContinuousFunction const_raw const_mu.
 Proof.
  unfold is_UniformlyContinuousFunction; now intuition.
 Qed.

const_uc c defines the uniformly continuous function λ _, c
 Open Scope uc_scope.
 Definition const_uc : X --> Complete X :=
   Build_UniformlyContinuousFunction (const_uc_prf).
End const_fun_uc.

Implicit Arguments const_uc [[X]].