Theorem Metric.externalCoveringNumber_eq_one_of_ediam_le

Modification history

2025-12-17 16:44
Mathlib/Topology/MetricSpace/CoveringNumbers.lean
feat: covering and packing numbers of sets in a metric space (#26351) …
Added Metric.externalCoveringNumber_eq_one_of_ediam_leView on Github →