Commit 2025-12-17 16:44 2fb75e07

View on Github →

feat: covering and packing numbers of sets in a metric space (#26351) We define covering numbers of sets in a pseudo-metric space, which are minimal cardinalities of ε-covers of sets. We also define the packing number, which is the maximal cardinality of an ε-separated set. From the Brownian motion project.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/CoveringNumbers.lean

added theorem Metric.IsCover.coveringNumber_le_encard

added theorem Metric.IsCover.externalCoveringNumber_le_encard

added def Metric.coveringNumber

added theorem Metric.coveringNumber_anti

added theorem Metric.coveringNumber_empty

added theorem Metric.coveringNumber_eq_one_of_ediam_le

added theorem Metric.coveringNumber_eq_zero

added theorem Metric.coveringNumber_le_one_of_ediam_le

added theorem Metric.coveringNumber_pos

added def Metric.externalCoveringNumber

added theorem Metric.externalCoveringNumber_anti

added theorem Metric.externalCoveringNumber_empty

added theorem Metric.externalCoveringNumber_eq_one_of_ediam_le

added theorem Metric.externalCoveringNumber_eq_zero

added theorem Metric.externalCoveringNumber_le_coveringNumber

added theorem Metric.externalCoveringNumber_le_one_of_ediam_le

added theorem Metric.externalCoveringNumber_mono_set

added theorem Metric.externalCoveringNumber_pos

added def Metric.packingNumber

added theorem Metric.packingNumber_two_mul_le_externalCoveringNumber