Commit 2024-07-21 19:24 f807a98a
View on Github →feat(MeasureTheory/Function): stronger version of Vitali's convergence theorem (#9163)
Prove a stronger version of Vitali's convergence theorem, which does not require an IsFiniteMeasure hypothesis. Instead it uses a new uniform tightness hypothesis. The hypothesis UnifTight is implemented closely following the structure of the existing UnifIntegrable.