Stream: math-comp analysis

Topic: `nondecreasing_cvg`


view this post on Zulip Cyril Cohen (May 25 2020 at 21:12):

@affeldt-aist, after thinking a bit more, we could reprove nondecreasing_cvg thanks to:

Lemma nondecreasing_cvg (u_ : {ereal R}^nat) (M : R) :   nondecreasing_seq u_ ->  u_ --> esup (u_ @` setT).

on one hand and lim_le on the other hand.


Last updated: Aug 19 2022 at 20:03 UTC