proposition: Lemma is_upper_bound_glb : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop), sig_not_dec_T -> sig_forall_dec_T -> (exists x : CRcarrier R, E x) -> (exists x : CRcarrier R, is_upper_bound E x) -> { x : CRcarrier R | forall r:Q, (x < CR_of_Q R r -> is_upper_bound E (CR_of_Q R r)) /\ (CR_of_Q R r < x -> ~is_upper_bound E (CR_of_Q R r)) }.
proof: Proof. intros R E sig_not_dec lpo Einhab Ebound. destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba]. destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) as [b glbb]. pose (fun q => is_upper_bound E (CR_of_Q R q)) as upcut. assert (forall q:Q, { upcut q } + { ~upcut q } ). { intro q. apply is_upper_bound_dec. - exact lpo. - exact sig_not_dec. } assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r). { intros. intros x Ex. specialize (H1 x Ex). intro abs. apply H1. apply (CRle_lt_trans _ (CR_of_Q R r)). 2: exact abs. apply CR_of_Q_le. exact H0. } assert (upcut (Z.of_nat a # 1)%Q). { intros x Ex. exact (luba x Ex). } assert (~upcut (- Z.of_nat b # 1)%Q). { intros abs. apply glbb. intros x Ex. specialize (abs x Ex). rewrite <- CR_of_Q_opp. exact abs. } assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r). { intros. intros x Ex. specialize (H4 x Ex). rewrite <- H3. exact H4. } destruct (@glb_dec_Q R (Build_DedekindDecCut upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1) H H0 H1 H2)). simpl in a0. exists x. intro r. split. - intros. apply a0. exact H4. - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0. + exact H6. + exact abs. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon