Commit 2023-11-08 01:47 2956f07e

View on Github →

feat(Topology/MetricSpace): weaker TC assumptions (#8259) Assume [WeaklyLocallyCompactSpace α] instead of [LocallyCompactSpace α] in 2 lemmas.

Estimated changes

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

modified theorem Metric.eventually_isCompact_closedBall

modified theorem Metric.exists_isCompact_closedBall