mathlib3

1c521b4f - feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767)

feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767) split from #17719 Co-authored-by: loefflerd <d.loeffler.01@cantab.net> Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>