Theorem MeasureTheory.tendstoInMeasure_of_ne_top

Modification history

2025-07-18 23:04

Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

chore: generalize `tendstoInMeasure_of_ne_top` (#27251) …

Modified MeasureTheory.tendstoInMeasure_of_ne_top View on Github →

2025-07-16 09:17

Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

chore: use `edist` instead of `dist` in `TendstoInMeasure` (#26954) …

Added MeasureTheory.tendstoInMeasure_of_ne_top View on Github →