Theorem MeasureTheory.OuterMeasure.mkMetric_mono

Modification history

2026-07-01 06:16
Mathlib/MeasureTheory/Measure/Hausdorff.lean
feat(Order): `Ici (1 : α) = univ` when `IsBotOneClass α` (#40762) …
Modified MeasureTheory.OuterMeasure.mkMetric_monoView on Github →
2023-06-11 14:32
Mathlib/MeasureTheory/Measure/Hausdorff.lean
feat: port MeasureTheory.Measure.Hausdorff (#4886)
Added MeasureTheory.OuterMeasure.mkMetric_monoView on Github →