Commit 2021-01-09 12:23 3166f4ef

View on Github →

feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523) These lemmas form part of a simplification of the proofs of #5361.

Estimated changes

Modified src/topology/metric_space/basic.lean

added theorem metric.exists_ball_inter_eq_singleton_of_mem_discrete

added theorem metric.exists_closed_ball_inter_eq_singleton_of_discrete

Modified src/topology/separation.lean

added theorem disjoint_nhds_within_of_mem_discrete

added theorem filter.has_basis.exists_inter_eq_singleton_of_mem_discrete

added theorem nhds_inter_eq_singleton_of_mem_discrete

added theorem nhds_within_of_mem_discrete

added theorem singleton_mem_nhds_within_of_mem_discrete