Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-12 06:59 1c521b4f

View on Github →

feat(topology): zero_at_infty_continuous_maps are uniform_continuous (#17767) split from #17719

Estimated changes

Modified src/topology/continuous_function/zero_at_infty.lean

added theorem zero_at_infty_continuous_map.uniform_continuous

Modified src/topology/uniform_space/basic.lean

added theorem exists_mem_nhds_ball_subset_of_mem_nhds

Modified src/topology/uniform_space/compact.lean

added theorem continuous.uniform_continuous_of_zero_at_infty

added theorem is_compact.uniform_continuous_at_of_continuous_at