Mathlib Changelog
v4
Changelog
About
Github
Theorem
Metric.IsSeparated.encard_le_packingNumber
Modification history
2025-12-19 15:12
Mathlib/Topology/MetricSpace/CoveringNumbers.lean
feat: API lemmas for covering and packing numbers (#33090) …
Added
Metric.IsSeparated.encard_le_packingNumber
View on Github →