Commit 2025-07-16 09:17 00a89835

View on Github →

chore: use edist instead of dist in TendstoInMeasure (#26954) With this change, we can use TendstoInMeasure in an extended metric space. Useful for the Brownian motion project.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

modified theorem MeasureTheory.TendstoInMeasure.comp

modified theorem MeasureTheory.TendstoInMeasure.mono

modified def MeasureTheory.TendstoInMeasure

modified theorem MeasureTheory.tendstoInMeasure_ae_unique

added theorem MeasureTheory.tendstoInMeasure_iff_dist

added theorem MeasureTheory.tendstoInMeasure_iff_enorm

modified theorem MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal

added theorem MeasureTheory.tendstoInMeasure_of_ne_top