Theorem Metric.coveringNumber_eq_one_of_ediam_le

Modification history

2026-01-06 17:14
Mathlib/Topology/MetricSpace/CoveringNumbers.lean
refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558) …
Modified Metric.coveringNumber_eq_one_of_ediam_leView 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.coveringNumber_eq_one_of_ediam_leView on Github →