Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 03:38 d11d83ad

View on Github →

feat(measure_theory/lebesgue_measure): volume of a box in ℝⁿ (#5635)

Estimated changes

Modified src/data/real/ennreal.lean

modified theorem ennreal.coe_nat

modified theorem ennreal.nat_ne_top

added theorem ennreal.of_real_coe_nat

modified theorem ennreal.top_ne_nat

Modified src/data/real/nnreal.lean

added theorem nnreal.mk_coe_nat

added theorem nnreal.of_real_coe_nat

Modified src/measure_theory/lebesgue_measure.lean

added theorem real.volume_Icc_pi

added theorem real.volume_Icc_pi_to_real

added theorem real.volume_Ici

added theorem real.volume_Iic

added theorem real.volume_Iio

added theorem real.volume_Ioi

added theorem real.volume_pi_Ico

added theorem real.volume_pi_Ico_to_real

added theorem real.volume_pi_Ioc

added theorem real.volume_pi_Ioc_to_real

added theorem real.volume_pi_Ioo

added theorem real.volume_pi_Ioo_to_real

Modified src/measure_theory/pi.lean

deleted theorem measure_theory.measure_space.pi_def

modified theorem measure_theory.volume_pi

added theorem measure_theory.volume_pi_pi