Commit 2026-04-30 16:36 5adee3bd

View on Github →

feat(MeasureTheory): use pseudometric in measurableSet_exists_tendsto (#38697)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

modified theorem MeasureTheory.measurableSet_exists_tendsto

Modified Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean

modified theorem MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

modified theorem stronglyMeasurable_iff_measurable