Stream: math-comp analysis

Topic: `nondecreasing_cvg`

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: Feb 05 2023 at 07:03 UTC