Theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero

Modification history

2024-08-16 08:13
Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean
feat(Measure/ContinuousPreimage): new file (#15367) …
Modified MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zeroView on Github →
2024-07-18 04:27
Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean
feat(LpSpace/ContinuousCompMeasurePreserving): new file (#14500) …
Added MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zeroView on Github →