proposition: Lemma is_sup_seq_lub (u : nat -> Rbar) (l : Rbar) : is_sup_seq u l -> Rbar_is_lub (fun x => exists n, x = u n) l.
proof: Proof. destruct l as [l | | ] ; intro Hl ; split. intro x ; destruct x as [x | | ] ; simpl ; intros (n, Hn). apply le_epsilon ; intros e He ; set (eps := mkposreal e He). change (Rbar_le x (l + e)). rewrite Hn ; apply Rbar_lt_le, (Hl eps). now generalize (proj1 (Hl (mkposreal _ Rlt_0_1)) n) ; clear Hl ; simpl ; intros Hl ; rewrite <-Hn in Hl. easy. intros b ; destruct b as [b | | ] ; intros Hb ; apply Rbar_not_lt_le ; auto ; intros He. set (eps := mkposreal _ (Rlt_Rminus _ _ He)) ; case (proj2 (Hl eps)) ; clear Hl ; intros n. apply Rbar_le_not_lt ; assert (l - eps = b) . simpl ; ring. rewrite H ; clear H ; apply Hb ; exists n ; auto. generalize (Rbar_ub_m_infty _ Hb) ; clear Hb ; intros Hb. case (proj2 (Hl (mkposreal _ Rlt_0_1))) ; clear Hl ; simpl ; intros n Hl. assert (H : (exists n0 : nat, u n = u n0)). exists n ; auto. generalize (Hb (u n) H) Hl ; clear Hb ; now case (u n). apply Rbar_ub_p_infty. intro b ; destruct b as [b | | ] ; simpl ; intro Hb. case (Hl b) ; clear Hl ; intros n Hl. contradict Hl ; apply Rbar_le_not_lt, Hb ; exists n ; auto. easy. generalize (Rbar_ub_m_infty _ Hb) ; clear Hb ; intro Hb. case (Hl 0) ; clear Hl; intros n Hl. assert (H : (exists n0 : nat, u n = u n0)). exists n ; auto. generalize (Hb (u n) H) Hl ; clear Hl ; now case (u n). intro x ; destruct x as [x | | ] ; intros (n, Hx). generalize (Hl x n) ; clear Hl ; intro Hl ; rewrite <-Hx in Hl ; apply Rlt_irrefl in Hl ; intuition. generalize (Hl 0 n) ; rewrite <-Hx ; intuition. easy. now intros b ; destruct b as [b | | ]. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy