proposition: Lemma sig_lub : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop), sig_forall_dec_T -> sig_not_dec_T -> (exists x : CRcarrier R, E x) -> (exists x : CRcarrier R, is_upper_bound E x) -> { u : CRcarrier R | is_lub E u }.
proof: Proof. intros R E sig_forall_dec sig_not_dec Einhab Ebound. pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound). destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H. exists x. exact H. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon