Monotone convergence theorem

Stream: mathlib4

[Junqi Liu]

Is there a monotone convergence theorem and DCT in mathlib4?

[Vincent Beffara]

Monotone convergence is docs#MeasureTheory.integral_tendsto_of_tendsto_of_monotone

DCT is docs#MeasureTheory.tendsto_integral_of_dominated_convergence

BTW one is spelled as integral_tendsto and the other one as tendsto_integral which is a bit weird...