mathlib

23f449bd - feat(topology/metric_space/basic): add closed_ball_mem_nhds (#3305)

feat(topology/metric_space/basic): add closed_ball_mem_nhds (#3305) I found this lemma handy when converting between the epsilon-N definition of convergence and the filter definition