mathlib3

0f79668f - feat(measure_theory/function/uniform_integrable): Egorov's theorem (#11328)

feat(measure_theory/function/uniform_integrable): Egorov's theorem (#11328) This PR proves Egorov's theorem which is necessary for the Vitali convergence theorem which is vital for the martingale convergence theorems.