Commit 2021-10-24 03:33 49c68412

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.