The lower Lebesgue integral

Monotone convergence theorem -- somtimes called Beppo-Levi convergence.

See lintegral_supr_directed for a more general form.

Weaker version of the monotone convergence theorem

Monotone convergence theorem for nonincreasing sequences of functions

Known as Fatou's lemma

Dominated convergence theorem for nonnegative functions

Monotone convergence for a suprema over a directed family and indexed by an encodable type