Commit 2025-12-19 15:12 fef749bb

View on Github →

feat: API lemmas for covering and packing numbers (#33090) Covering and packing numbers of empty sets and singletons.

Estimated changes

Modified Mathlib/Topology/MetricSpace/CoveringNumbers.lean

added theorem Metric.IsSeparated.encard_le_packingNumber

added theorem Metric.coveringNumber_le_encard_self

deleted theorem Metric.coveringNumber_pos

added theorem Metric.coveringNumber_pos_iff

added theorem Metric.coveringNumber_singleton

added theorem Metric.coveringNumber_zero

added theorem Metric.externalCoveringNumber_le_encard_self

deleted theorem Metric.externalCoveringNumber_pos

added theorem Metric.externalCoveringNumber_pos_iff

added theorem Metric.externalCoveringNumber_singleton

added theorem Metric.externalCoveringNumber_zero

added theorem Metric.packingNumber_empty

added theorem Metric.packingNumber_eq_zero

added theorem Metric.packingNumber_le_encard_self

added theorem Metric.packingNumber_pos_iff

added theorem Metric.packingNumber_singleton

added theorem Metric.packingNumber_zero

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean

added theorem Metric.isSeparated_zero