Theorem MeasureTheory.hausdorffMeasure_orthogonalProjection_le

Modification history

2025-06-20 12:59
Mathlib/MeasureTheory/Measure/Hausdorff.lean
feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection (#25759) …
Added MeasureTheory.hausdorffMeasure_orthogonalProjection_leView on Github →