Theorem MeasureTheory.measureReal_diff_null'

Modification history

2026-06-09 08:51

Mathlib/MeasureTheory/Measure/Real.lean

chore: rename `diff` to `sdiff` (#40184) …

Deleted MeasureTheory.measureReal_diff_null'View on Github →

2025-04-11 19:15

Mathlib/MeasureTheory/Measure/Real.lean

feat: `μ.real` as the real-valued version of a measure (#23943) …

Added MeasureTheory.measureReal_diff_null'View on Github →