Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_inter_eq_singleton_of_mem_discrete

Modification history

2021-01-14 08:39
src/topology/separation.lean
chore(*): split some long lines (#5742)
Modified nhds_inter_eq_singleton_of_mem_discreteView on Github →
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_inter_eq_singleton_of_mem_discreteView on Github →