Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_mem_nhds_ball_subset_of_mem_nhds

Modification history

2022-12-12 06:59
src/topology/uniform_space/basic.lean
feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767) …
Added exists_mem_nhds_ball_subset_of_mem_nhdsView on Github →