Theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete
Modification history
2024-08-16 01:08
Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
chore: splitting up metric spaces files (#15790)
Modified Metric.exists_closedBall_inter_eq_singleton_of_discreteView on Github →