Commit 2025-11-05 13:09 f84aa9af

View on Github →

feat(MetricSpace): covers (aka nets) (#23124) Define covers (aka nets), which are a quantitative notion of compactness in a metric space. From my PhD (MiscYD)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Cover.lean

added theorem Metric.IsCover.isCompact

added theorem Metric.IsCover.isCompact_closure

added theorem Metric.IsCover.mono_radius

added theorem Metric.IsCover.of_subset_cthickening_of_lt

added def Metric.IsCover

added theorem Metric.exists_finite_isCover_of_isCompact

added theorem Metric.exists_finite_isCover_of_isCompact_closure

added theorem Metric.isCompact_closure_iff_exists_finite_isCover

added theorem Metric.isCover_closure

added theorem Metric.isCover_iff_subset_cthickening

added theorem Metric.isCover_iff_subset_iUnion_closedBall

added theorem Metric.isCover_iff_subset_iUnion_emetricClosedBall

added theorem Metric.isCover_zero

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean

added theorem Metric.isSeparated_iff_setRelIsSeparated