chore(topology/metric_space/basic): golf, add dot notation (#11111)
chore(topology/metric_space/basic): golf, add dot notation (#11111)

* add `cauchy_seq.bounded_range`;
* golf `metric.bounded_range_of_tendsto`.





leanprover-community/mathlib,leanprover-community/mathlib