Def MeasureTheory.TendstoInMeasure

Modification history

2025-07-16 09:17
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
chore: use `edist` instead of `dist` in `TendstoInMeasure` (#26954) …
Modified MeasureTheory.TendstoInMeasureView on Github →
2023-06-01 12:52
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
feat: port MeasureTheory.Function.ConvergenceInMeasure (#4484)
Added MeasureTheory.TendstoInMeasureView on Github →