proposition: Lemma totally_bounded_has_glb : forall P : IR -> CProp, totally_bounded P -> {z : IR | set_glb_IR P z}.
proof: Proof. intros P tot_bnd. red in tot_bnd. elim tot_bnd; intros non_empty H. cut {sequence : nat -> IR | forall k : nat, P (sequence k) | forall (k : nat) (x : IR), P x -> sequence k[-]x [<=] Two[*]one_div_succ k}. intros H0. elim H0. clear H0; intros seq H0 H1. cut (Cauchy_prop seq). intro H2. set (seq1 := Build_CauchySeq IR seq H2) in *. exists (Lim seq1). split; intros. apply shift_leEq_rht. astepl ( [--]ZeroR); rstepr ( [--] (Lim seq1[-]x)). apply inv_resp_leEq. set (seq2 := Cauchy_const x) in *. apply leEq_wdl with (Lim seq1[-]Lim seq2). 2: apply cg_minus_wd; [ algebra | unfold seq2 in |- *; apply eq_symmetric_unfolded; apply Lim_const ]. apply leEq_wdl with (Lim (Build_CauchySeq IR (fun n : nat => seq1 n[-]seq2 n) (Cauchy_minus seq1 seq2))). apply leEq_transitive with (Lim twice_inv_seq). apply Lim_leEq_Lim; intro. simpl in |- *. apply H1; assumption. apply eq_imp_leEq. apply eq_symmetric_unfolded; apply Limits_unique. red in |- *; fold (SeqLimit twice_inv_seq [0]) in |- *. apply twice_inv_seq_Lim. apply Lim_minus. cut (Cauchy_Lim_prop2 seq (Lim seq1)). intro H4; red in H4. try rename X into H3. elim (H4 (e [/]TwoNZ) (pos_div_two _ _ H3)); clear H4. intros n Hn. exists (seq n). apply H0. apply leEq_less_trans with (AbsIR (Lim seq1[-]seq n)). rstepl ( [--] (Lim seq1[-]seq n)). apply inv_leEq_AbsIR. apply leEq_less_trans with (e [/]TwoNZ). apply AbsSmall_imp_AbsIR. apply AbsSmall_minus; simpl in |- *; apply Hn. apply le_n. apply pos_div_two'; auto. cut (Cauchy_Lim_prop2 seq1 (Lim seq1)); intros. try rename X0 into H4. red in |- *; red in H4. intros eps Heps; elim (H4 eps Heps); clear H4; intros. exists x. intros m Hm; elim (p m Hm); clear p. intros. astepr (seq1 m[-]Lim seq1). apply AbsIR_eq_AbsSmall; assumption. red in |- *; fold (SeqLimit seq1 (Lim seq1)) in |- *. apply ax_Lim. apply crl_proof. red in |- *; intros e H2. elim (Archimedes ([1][/] e[//]pos_ap_zero _ _ H2)). intros n Hn. exists (S (2 * n)); intros. cut ([0] [<] nring (R:=IR) n); intros. apply AbsIR_eq_AbsSmall. try rename X into H4. apply leEq_transitive with ( [--] ([1][/] nring n[//]pos_ap_zero _ _ H4)). apply inv_resp_leEq. apply shift_div_leEq. assumption. eapply shift_leEq_mult'; [ assumption | apply Hn ]. apply less_leEq. rstepr ( [--] (seq (S (2 * n)) [-]seq m)); apply inv_resp_less. apply leEq_less_trans with (Two[*]one_div_succ (R:=IR) (S (2 * n))). apply H1; apply H0. astepl (one_div_succ (R:=IR) (S (2 * n)) [*]Two). unfold one_div_succ in |- *; unfold Snring in |- *. apply shift_mult_less with (two_ap_zero IR). apply pos_two. rstepr ([1][/] Two[*]nring n[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (pos_ap_zero _ _ H4)). apply recip_resp_less. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; [ apply pos_two | assumption ]. apply less_wdr with (Two[*]nring (R:=IR) n[+][1][+][1]). apply less_transitive_unfolded with (Two[*]nring (R:=IR) n[+][1]); apply less_plusOne. astepr (nring (R:=IR) (S (2 * n)) [+][1]). Step_final (nring (R:=IR) (2 * n) [+][1][+][1]). apply leEq_transitive with (Two[*]one_div_succ (R:=IR) m). apply H1; apply H0. apply leEq_transitive with (one_div_succ (R:=IR) n). unfold one_div_succ in |- *. unfold Snring in |- *. rstepl ([1][/] nring (R:=IR) (S m) [/]TwoNZ[//] div_resp_ap_zero_rev _ _ _ _ (nring_ap_zero IR (S m) (sym_not_eq (O_S m)))). apply recip_resp_leEq. apply pos_nring_S. apply shift_leEq_div. apply pos_two. simpl in |- *; fold (Two:IR) in |- *. rstepl (Two[*]nring (R:=IR) n[+][1][+][1]). apply plus_resp_leEq. apply leEq_wdl with (nring (R:=IR) (S (2 * n))). apply nring_leEq; assumption. Step_final (nring (R:=IR) (2 * n) [+][1]). unfold one_div_succ in |- *; unfold Snring in |- *. rstepr ([1][/] [1][/] e[//]pos_ap_zero _ _ H2[//] div_resp_ap_zero_rev _ _ _ _ (one_ap_zero IR)). apply recip_resp_leEq. apply recip_resp_pos; assumption. apply leEq_transitive with (nring (R:=IR) n); [ assumption | simpl in |- *; apply less_leEq; apply less_plusOne ]. eapply less_leEq_trans. 2: apply Hn. apply recip_resp_pos; assumption. elim (aux_seq_glb_prop P tot_bnd). exists (fun k : nat => scs_elem _ _ (aux_seq_glb P tot_bnd k)); auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists