Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.exists_ball_inter_eq_singleton_of_mem_discrete

Modification history

2021-01-09 12:23
src/topology/metric_space/basic.lean
feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523) …
Added metric.exists_ball_inter_eq_singleton_of_mem_discreteView on Github →