Example of a real number structure: ⟨CR⟩


Lemma CRAbsSmall_ball : forall (x y:CR) (e:Qpos), AbsSmall (R:=CRasCOrdField) (inject_Q e) ((x:CRasCOrdField)[-]y) <->
 ball e x y.

Lemma CRlt_Qlt : forall a b, (a < b)%Q -> ((' a%Q) < (' b))%CR.

Definition CRlim (s:CauchySeq CRasCOrdField) : CR.
Defined.

Lemma CRisCReals : is_CReals CRasCOrdField CRlim.

Definition CRasCReals : CReals :=
Build_CReals _ _ CRisCReals.

Canonical Structure CRasCReals.