Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 17:29 777d1ec1

View on Github →

feat(measure_theory/measure/measure_space): add some lemmas for the counting measure (#13485)

Estimated changes

Modified src/measure_theory/measure/measure_space.lean

modified theorem measure_theory.measure.count_apply_eq_top

modified theorem measure_theory.measure.count_apply_lt_top

added theorem measure_theory.measure.count_empty

added theorem measure_theory.measure.count_eq_zero_iff

added theorem measure_theory.measure.count_ne_zero

added theorem measure_theory.measure.count_singleton

added theorem measure_theory.measure.empty_of_count_eq_zero