basic): add lemma `exists_lt_mem_ball_of_mem_ball` (#14627)

Commit

3 years ago

feat(topology/metric_space/basic): add lemma `exists_lt_mem_ball_of_mem_ball` (#14627) This is apparently necessary in https://github.com/leanprover-community/mathlib/pull/13885

Author

ocfnash

Parents

6a1ce4e8

mathlib bc7b3425 - feat(topology/metric_space/basic): add lemma `exists_lt_mem_ball_of_mem_ball` (#14627)

mathlib
bc7b3425 - feat(topology/metric_space/basic): add lemma `exists_lt_mem_ball_of_mem_ball` (#14627)