Theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall

Modification history

2024-12-26 07:24
Mathlib/MeasureTheory/Covering/Vitali.lean
docs: fix typos across repository (#20239) …
Deleted Vitali.exists_disjoint_subfamily_covering_enlargment_closedBallView on Github →
2024-10-14 06:05
Mathlib/MeasureTheory/Covering/Vitali.lean
chore: weaken typeclass assumptions `MetricSpace` → `PseudoMetricSpace` (#17520) …
Modified Vitali.exists_disjoint_subfamily_covering_enlargment_closedBallView on Github →
2023-05-22 03:13
Mathlib/MeasureTheory/Covering/Vitali.lean
feat: port MeasureTheory.Covering.Vitali (#4178)
Added Vitali.exists_disjoint_subfamily_covering_enlargment_closedBallView on Github →