Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_within_of_mem_discrete

Modification history

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