Theorem Vitali.exists_disjoint_covering_ae

Modification history

2024-10-14 06:05

Mathlib/MeasureTheory/Covering/Vitali.lean

chore: weaken typeclass assumptions `MetricSpace` → `PseudoMetricSpace` (#17520) …

Modified Vitali.exists_disjoint_covering_ae View on Github →

2023-05-22 03:13

Mathlib/MeasureTheory/Covering/Vitali.lean

feat: port MeasureTheory.Covering.Vitali (#4178)

Added Vitali.exists_disjoint_covering_ae View on Github →