Commit 2024-03-13 17:36 d048b949

View on Github →

feat(MetricSpace): add tendsto_closedBall_smallSets (#11068) Use it to golf Vitali.exists_disjoint_covering_ae

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

added theorem tendsto_closedBall_smallSets