mathlib3

bfccd1b8 - chore(topology/{metric_space,instances/real}): cleanup (#10577)

chore(topology/{metric_space,instances/real}): cleanup (#10577) * merge `real.ball_eq` and `real.ball_eq_Ioo` into `real.ball_eq_Ioo`; * merge `real.closed_ball_eq` and `real.closed_ball_eq_Icc` into `real.closed_ball_eq_Icc`; * add missing `real.Icc_eq_closed_ball`; * generalize lemmas about `*bounded_Ixx` so that they work for (indexed) products of conditionally complete linear orders.