Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subsingleton.measure_zero

Modification history

2021-08-22 13:58

src/measure_theory/measure/measure_space.lean

chore(measure_theory): make `μ` an explicit argument in `subsingleton.measure_zero` etc (#8793)

Added set.subsingleton.measure_zero View on Github →