CoRN.reals.fast.CRconst
Require Import Unicode.Utf8 Qmetric CRmetric UniformContinuity.
Section const_fun_uc.
Variable X : MetricSpace.
Variable c : X.
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.
Definition const_mu (ε:Qpos) : QposInf := QposInfinity.
Lemma const_uc_prf : is_UniformlyContinuousFunction const_raw const_mu.
Proof.
unfold is_UniformlyContinuousFunction; now intuition.
Qed.
Open Scope uc_scope.
Definition const_uc : X --> Complete X :=
Build_UniformlyContinuousFunction (const_uc_prf).
End const_fun_uc.
Implicit Arguments const_uc [[X]].
Definition const_uc : X --> Complete X :=
Build_UniformlyContinuousFunction (const_uc_prf).
End const_fun_uc.
Implicit Arguments const_uc [[X]].