Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-26 12:04 74b96471

View on Github →

feat(measure_theory/measure_space): pigeonhole principle in a measure space (#2538) ref #2272

Estimated changes

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.exists_nonempty_inter_of_volume_univ_lt_sum_volume

added theorem measure_theory.exists_nonempty_inter_of_volume_univ_lt_tsum_volume

added theorem measure_theory.sum_volume_le_volume_univ

added theorem measure_theory.tsum_volume_le_volume_univ