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