Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-23 17:55 8a7e4f74

View on Github →

feat(measure_theory): volume of a (closed) L∞-ball (#8791)

pi measure of a (closed or open) ball;
volume of a (closed or open) ball in
- Π i, α i;
- ℝ;
- ι → ℝ;
volumes of univ, emetric.ball, and emetric.closed_ball in ℝ.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_pow

Modified src/measure_theory/constructions/pi.lean

added theorem measure_theory.measure.pi_ball

added theorem measure_theory.measure.pi_closed_ball

added theorem measure_theory.volume_pi_ball

added theorem measure_theory.volume_pi_closed_ball

Modified src/measure_theory/measure/lebesgue.lean

added theorem real.volume_ball

added theorem real.volume_closed_ball

added theorem real.volume_emetric_ball

added theorem real.volume_emetric_closed_ball

added theorem real.volume_pi_ball

added theorem real.volume_pi_closed_ball

added theorem real.volume_univ