Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 08:06 2b435875

View on Github →

feat(measure_theory/hausdorff_measure): Hausdorff measure and volume coincide in pi types (#8554) co-authored by Yury Kudryashov

Estimated changes

Modified src/measure_theory/measure/hausdorff.lean

added theorem measure_theory.hausdorff_measure_pi_real

added theorem measure_theory.measure.hausdorff_measure_le

added theorem measure_theory.measure.le_hausdorff_measure

added theorem measure_theory.measure.le_mk_metric

added theorem measure_theory.outer_measure.le_mk_metric