mathlib

12bbd533 - chore(topology/metric_space/basic): add `metric.uniform_continuous_on_iff_le` (#8906)

chore(topology/metric_space/basic): add `metric.uniform_continuous_on_iff_le` (#8906) This is a version of `metric.uniform_continuous_on_iff` with `≤ δ` and `≤ ε` instead of `< δ` and `< ε`. Also golf the proof of `metric.uniform_continuous_on_iff`.