chore(topology): generalize `real.image_Icc` etc (#9784)
* add lemmas about `Ici`/`Iic`/`Icc` in `α × β`;
* introduce a typeclass for `is_compact_Icc` so that the same lemma works for `ℝ` and `ℝⁿ`;
* generalize `real.image_Icc` etc to a conditionally complete linear order (e.g., now it works for `nnreal`, `ennreal`, `ereal`), move these lemmas to the `continuous_on` namespace.
