Commit 2021-12-03 08:57 bfccd1b8

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.