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: Jun 25 2024 at 19:01 UTC