Theorem Metric.externalCoveringNumber_pos

Modification history

2025-12-19 15:12
Mathlib/Topology/MetricSpace/CoveringNumbers.lean
feat: API lemmas for covering and packing numbers (#33090) …
Deleted Metric.externalCoveringNumber_posView on Github →
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_posView on Github →