proposition: Lemma is_upper_bound_closed : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop) (sig_forall_dec : sig_forall_dec_T) (sig_not_dec : sig_not_dec_T) (Einhab : exists x : CRcarrier R, E x) (Ebound : exists x : CRcarrier R, is_upper_bound E x), is_lub E (proj1_sig (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound)).
proof: Proof. intros. split. - intros x Ex. destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl. intro abs. destruct (CR_Q_dense R x0 x abs) as [q [qmaj H]]. specialize (a q) as [a _]. specialize (a qmaj x Ex). contradiction. - intros. destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl. intro abs. destruct (CR_Q_dense R b x abs) as [q [qmaj H0]]. specialize (a q) as [_ a]. apply a. + exact H0. + intros y Ey. specialize (H y Ey). intro abs2. apply H. exact (CRlt_trans _ (CR_of_Q R q) _ qmaj abs2). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon