proposition: Lemma Rbar_is_lub_sup_seq (u : nat -> Rbar) (l : Rbar) : Rbar_is_lub (fun x => exists n, x = u n) l -> is_sup_seq u l.
proof: Proof. destruct l as [l | | ] ; intros (ub, lub). intro eps ; split. intro n ; apply Rbar_le_lt_trans with (y := Finite l). apply ub ; exists n ; auto. pattern l at 1 ; rewrite <-(Rplus_0_r l) ; apply Rplus_lt_compat_l, eps. apply LPO_notforall. intro n. destruct (Rbar_lt_dec (l - eps) (u n)) as [H|H]. now left. now right. intro H. assert (H0 : (Rbar_is_upper_bound (fun x : Rbar => exists n : nat, x = u n) (Finite (l - eps)))). intros x (n,Hn) ; rewrite Hn ; clear Hn ; apply Rbar_not_lt_le, H. generalize (lub _ H0) ; clear lub ; apply Rbar_lt_not_le ; pattern l at 2 ; rewrite <-(Rplus_0_r l) ; apply Rplus_lt_compat_l, Ropp_lt_gt_0_contravar, eps. intro M ; apply LPO_notforall. intro n. destruct (Rbar_lt_dec M (u n)) as [H|H]. now left. now right. intro H. assert (H0 : Rbar_is_upper_bound (fun x : Rbar => exists n : nat, x = u n) (Finite M)). intros x (n,Hn) ; rewrite Hn ; clear Hn ; apply Rbar_not_lt_le, H. generalize (lub _ H0) ; clear lub ; apply Rbar_lt_not_le ; simpl ; auto. intros M n. apply Rbar_le_lt_trans with (y := m_infty) ; simpl ; auto. apply ub ; exists n ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy