2025-02-11 15:35
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
feat(MeasureTheory): TendstoInMeasure gives ae unique limits; TendstoInMeasure equivalent to subsequences converging ae (#14033) …
Added MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff