proposition: Lemma is_inf_seq_glb (u : nat -> Rbar) (l : Rbar) : is_inf_seq u l -> Rbar_is_glb (fun x => exists n, x = u n) l.
proof: Proof. move => H ; apply Rbar_lub_glb ; apply (Rbar_is_lub_ext (fun x : Rbar => exists n : nat, x = Rbar_opp (u n))). move => x ; split ; case => n Hn ; exists n. by rewrite Hn Rbar_opp_involutive. by rewrite -Hn Rbar_opp_involutive. apply (is_sup_seq_lub (fun n => Rbar_opp (u n)) (Rbar_opp l)) ; by apply is_sup_opp_inf_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy