Commit 2021-08-17 09:42 edb0ba42
View on Github →chore(measure_theory/measure/hausdorff): golf (#8706)
- add a
mk_metricversion ofhausdorff_measure_le, addfinset.sumversions for bothmk_metricandhausdorff_measure; - slightly golf the proof.
chore(measure_theory/measure/hausdorff): golf (#8706)
mk_metric version of hausdorff_measure_le, add finset.sum versions for both mk_metric and hausdorff_measure;