Theorem MeasureTheory.TendstoInMeasure.indicator

Modification history

2025-12-19 18:35
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable (#31886)
Added MeasureTheory.TendstoInMeasure.indicatorView on Github →